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

Theorem eqriv 2448
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-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 2445 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1673 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    = wceq 1444    e. wcel 1887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-cleq 2444
This theorem is referenced by:  eqid  2451  cbvab  2574  vjust  3046  nfccdeq  3265  difeqri  3553  uneqri  3576  incom  3625  ineqri  3626  symdifass  3672  indifdir  3699  undif3  3704  csbcom  3783  csbab  3797  pwpr  4194  pwtp  4195  pwv  4197  uniun  4217  intun  4267  intpr  4268  iuncom  4285  iuncom4  4286  iun0  4334  0iun  4335  iunin2  4342  iinun2  4344  iundif2  4345  iunun  4362  iunxun  4363  iunxiun  4364  iinpw  4370  inuni  4565  unipw  4650  xpiundi  4889  xpiundir  4890  0xp  4915  iunxpf  4983  cnvuni  5021  dmiun  5043  dmuni  5044  epini  5198  rniun  5246  xpdifid  5265  cnvresima  5324  imaco  5340  rnco  5341  dfmpt3  5698  imaiun  6150  snnex  6597  unon  6658  opabex3d  6771  opabex3  6772  fparlem1  6896  fparlem2  6897  oarec  7263  ecid  7428  qsid  7429  mapval2  7501  ixpin  7547  onfin2  7764  unfilem1  7835  unifpw  7877  dfom5  8155  alephsuc2  8511  ackbij2  8673  isf33lem  8796  dffin7-2  8828  fin1a2lem6  8835  acncc  8870  fin41  8874  iunfo  8964  grutsk  9247  grothac  9255  grothtsk  9260  dfz2  10955  qexALT  11279  om2uzrani  12166  hashkf  12517  divalglem4  14375  1nprm  14629  nsgacs  16853  oppgsubm  17013  oppgsubg  17014  oppgcntz  17015  pmtrprfvalrn  17129  opprsubg  17864  opprunit  17889  opprirred  17930  opprsubrg  18029  00lss  18165  00ply1bas  18833  dfprm2  19065  unocv  19243  iunocv  19244  unisngl  20542  zcld  21831  iundisj  22501  plyun0  23151  aannenlem2  23285  eqid1  25904  choc0  26979  chocnul  26981  spanunsni  27232  lncnbd  27691  adjbd1o  27738  rnbra  27760  pjimai  27829  rabtru  28135  iunin1f  28171  iundisjf  28199  dfrp2  28352  xrdifh  28362  iundisjfi  28372  cmpcref  28677  eulerpartgbij  29205  eulerpartlemr  29207  dfdm5  30418  dfrn5  30419  dffix2  30672  fixcnv  30675  dfom5b  30679  fnimage  30696  brimg  30704  bj-vjust  31401  bj-csbsnlem  31505  bj-projun  31588  finxp0  31783  finxp1o  31784  iundif1  31927  poimirlem26  31966  csbcom2fi  32369  csbgfi  32370  prtlem16  32441  aaitgo  36028  imaiun1  36243  nzss  36666  dfodd2  38766  dfeven5  38796  dfodd7  38797
  Copyright terms: Public domain W3C validator