MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqriv Unicode version

Theorem eqriv 2313
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqriv.1  |-  ( x  e.  A  <->  x  e.  B )
Assertion
Ref Expression
eqriv  |-  A  =  B
Distinct variable groups:    x, A    x, B

Proof of Theorem eqriv
StepHypRef Expression
1 dfcleq 2310 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1541 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1633    e. wcel 1701
This theorem is referenced by:  eqid  2316  cbvab  2434  vjust  2823  nfccdeq  3023  difeqri  3330  uneqri  3351  incom  3395  ineqri  3396  indifdir  3459  undif3  3463  pwpr  3860  pwtp  3861  pwv  3863  uniun  3883  intun  3931  intpr  3932  iuncom  3948  iuncom4  3949  iun0  3995  0iun  3996  iunin2  4003  iinun2  4005  iundif2  4006  iunun  4019  iunxun  4020  iunxiun  4021  iinpw  4027  inuni  4210  unipw  4261  pwundifOLD  4338  snnex  4561  unon  4659  xpiundi  4780  xpiundir  4781  xp0r  4805  iunxpf  4869  cnvuni  4903  dmiun  4924  dmuni  4925  epini  5080  rniun  5128  cnvresima  5199  imaco  5215  rnco  5216  dfmpt3  5403  opabex3d  5810  opabex3  5811  imaiun  5813  fparlem1  6260  fparlem2  6261  oarec  6602  ecid  6766  qsid  6767  mapval2  6840  ixpin  6884  onfin2  7095  unfilem1  7166  unifpw  7203  dfom5  7396  alephsuc2  7752  ackbij2  7914  isf33lem  8037  dffin7-2  8069  fin1a2lem6  8076  acncc  8111  fin41  8115  iunfo  8206  grutsk  8489  grothac  8497  grothtsk  8502  dfz2  10088  qexALT  10378  om2uzrani  11062  hashkf  11386  divalglem4  12642  1nprm  12810  nsgacs  14702  oppgsubm  14884  oppgsubg  14885  oppgcntz  14886  opprsubg  15467  opprunit  15492  opprirred  15533  opprsubrg  15615  00lss  15748  00ply1bas  16367  dfprm2  16503  unocv  16636  iunocv  16637  zcld  18371  iundisj  18958  plyun0  19632  aannenlem2  19762  eqid1  20893  choc0  21960  chocnul  21962  spanunsni  22213  lncnbd  22673  adjbd1o  22720  rnbra  22742  pjimai  22811  iundisjf  23171  xrdifh  23290  iundisjfi  23301  dfdm5  24517  dfrn5  24518  symdifass  24756  dffix2  24830  fixcnv  24833  dfom5b  24837  fnimage  24853  brimg  24861  cnvresimaOLD  25375  prtlem16  25885  aaitgo  26515
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-cleq 2309
  Copyright terms: Public domain W3C validator