Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem eqriv 1467

Description: Infer equality of classes from equivalence of membership.

Hypothesis

Ref	Expression
eqri.1

Assertion

Ref	Expression
eqriv

Distinct variable groups:   ,   ,

---

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 1463	. 2
2		eqri.1	. 2
3	1, 2	mpgbir 985	1

Colors of variables: wff set class

Syntax hints:   wb 146   wceq 953   wcel 955

This theorem is referenced by:  eqid 1468  uneqri 2164  uncom 2166  incom 2198  ineqri 2199  dfss4 2232  dfun2 2233  dfin2 2234  difin 2235  indi 2241  undi 2242  unab 2257  inab 2258  pwv 2492  uniun 2509  intun 2552  intpr 2553  iunid 2593  iun0 2594  0iun 2595  iunin2 2598  iinun2 2599  iundif2 2600  iunxsn 2602  iunxun 2604  iinuni 2605  iinpw 2607  pwundif 2817  unon 3078  xp0r 3229  cnvuni 3290  dmun 3306  dmuni 3308  rnuni 3445  imaco 3487  rnco 3488  imaiun 3849  erdmrn 4260  mapval2 4319  mapixp 4346  jech9.3 4638  dfn2 6059  dfuz 6150  om2uzran 6237  qnnen 7446  pilem1 8590  circgrp 8660  choc0 9205  chocnul 9207  spanunsn 9419  lncnbd 9882  adjbd1o 9933  rnbra 9953  pjima 10015  ntunte 10340  dtopcl 10459

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-cleq 1462

Copyright terms: Public domain