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

Theorem eqriv 2280
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 2277 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1537 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eqid  2283  cbvab  2401  vjust  2789  nfccdeq  2989  difeqri  3296  uneqri  3317  incom  3361  ineqri  3362  indifdir  3425  undif3  3429  pwpr  3823  pwtp  3824  pwv  3826  uniun  3846  intun  3894  intpr  3895  iuncom  3911  iuncom4  3912  iun0  3958  0iun  3959  iunin2  3966  iinun2  3968  iundif2  3969  iunun  3982  iunxun  3983  iunxiun  3984  iinpw  3990  inuni  4173  unipw  4224  pwundifOLD  4301  snnex  4524  unon  4622  xpiundi  4743  xpiundir  4744  xp0r  4768  iunxpf  4832  cnvuni  4866  dmiun  4887  dmuni  4888  epini  5043  rniun  5091  cnvresima  5162  imaco  5178  rnco  5179  dfmpt3  5366  opabex3  5769  imaiun  5771  fparlem1  6218  fparlem2  6219  oarec  6560  ecid  6724  qsid  6725  mapval2  6797  ixpin  6841  onfin2  7052  unfilem1  7121  unifpw  7158  dfom5  7351  alephsuc2  7707  ackbij2  7869  isf33lem  7992  dffin7-2  8024  fin1a2lem6  8031  acncc  8066  fin41  8070  iunfo  8161  grutsk  8444  grothac  8452  grothtsk  8457  dfz2  10041  qexALT  10331  om2uzrani  11015  hashkf  11339  divalglem4  12595  1nprm  12763  nsgacs  14653  oppgsubm  14835  oppgsubg  14836  oppgcntz  14837  opprsubg  15418  opprunit  15443  opprirred  15484  opprsubrg  15566  00lss  15699  00ply1bas  16318  dfprm2  16447  unocv  16580  iunocv  16581  zcld  18319  iundisj  18905  plyun0  19579  aannenlem2  19709  eqid1  20840  choc0  21905  chocnul  21907  spanunsni  22158  lncnbd  22618  adjbd1o  22665  rnbra  22687  pjimai  22756  xrdifh  23273  iundisjfi  23363  iundisjf  23365  dfdm5  24132  dfrn5  24133  symdifass  24371  dffix2  24445  fixcnv  24448  dfom5b  24452  fnimage  24468  brimg  24476  dstr  25171  cnvresimaOLD  26226  prtlem16  26737  aaitgo  27367
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator