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

Theorem eqriv 2439
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 2436 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1609 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1383    e. wcel 1804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  eqid  2443  cbvab  2584  cbvabOLD  2585  vjust  3096  nfccdeq  3311  difeqri  3609  uneqri  3631  incom  3676  ineqri  3677  indifdir  3739  undif3  3744  csbcom  3823  csbab  3841  pwpr  4230  pwtp  4231  pwv  4233  uniun  4253  intun  4304  intpr  4305  iuncom  4322  iuncom4  4323  iun0  4371  0iun  4372  iunin2  4379  iinun2  4381  iundif2  4382  iunun  4396  iunxun  4397  iunxiun  4398  iinpw  4404  inuni  4599  unipw  4687  xpiundi  5044  xpiundir  5045  0xp  5070  iunxpf  5141  cnvuni  5179  dmiun  5201  dmuni  5202  epini  5357  rniun  5406  xpdifid  5425  cnvresima  5486  imaco  5502  rnco  5503  dfmpt3  5693  imaiun  6142  snnex  6591  unon  6651  opabex3d  6763  opabex3  6764  fparlem1  6885  fparlem2  6886  oarec  7213  ecid  7378  qsid  7379  mapval2  7450  ixpin  7496  onfin2  7711  unfilem1  7786  unifpw  7825  dfom5  8070  alephsuc2  8464  ackbij2  8626  isf33lem  8749  dffin7-2  8781  fin1a2lem6  8788  acncc  8823  fin41  8827  iunfo  8917  grutsk  9203  grothac  9211  grothtsk  9216  dfz2  10888  qexALT  11206  om2uzrani  12042  hashkf  12386  divalglem4  13931  1nprm  14099  nsgacs  16111  oppgsubm  16271  oppgsubg  16272  oppgcntz  16273  pmtrprfvalrn  16387  opprsubg  17159  opprunit  17184  opprirred  17225  opprsubrg  17324  00lss  17462  00ply1bas  18155  dfprm2  18397  dfprm2OLD  18400  unocv  18584  iunocv  18585  unisngl  19901  zcld  21191  iundisj  21831  plyun0  22467  aannenlem2  22597  eqid1  25047  choc0  26116  chocnul  26118  spanunsni  26369  lncnbd  26829  adjbd1o  26876  rnbra  26898  pjimai  26967  iundisjf  27320  xrdifh  27463  iundisjfi  27473  cmpcref  27726  eulerpartgbij  28184  eulerpartlemr  28186  dfdm5  29181  dfrn5  29182  symdifass  29452  dffix2  29530  fixcnv  29533  dfom5b  29537  fnimage  29554  brimg  29562  iundif1  30012  csbcom2fi  30509  csbgfi  30510  prtlem16  30585  aaitgo  31087  nzss  31198  bj-vjust  34114  bj-csbsnlem  34212  bj-projun  34294
  Copyright terms: Public domain W3C validator