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

Theorem eqriv 2398
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 2395 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1643 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1405    e. wcel 1842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394
This theorem is referenced by:  eqid  2402  cbvab  2543  cbvabOLD  2544  vjust  3060  nfccdeq  3275  difeqri  3563  uneqri  3585  incom  3632  ineqri  3633  symdifass  3679  indifdir  3706  undif3  3711  csbcom  3788  csbab  3802  pwpr  4187  pwtp  4188  pwv  4190  uniun  4210  intun  4260  intpr  4261  iuncom  4278  iuncom4  4279  iun0  4327  0iun  4328  iunin2  4335  iinun2  4337  iundif2  4338  iunun  4355  iunxun  4356  iunxiun  4357  iinpw  4363  inuni  4556  unipw  4641  xpiundi  4878  xpiundir  4879  0xp  4904  iunxpf  4972  cnvuni  5010  dmiun  5032  dmuni  5033  epini  5187  rniun  5234  xpdifid  5253  cnvresima  5312  imaco  5328  rnco  5329  dfmpt3  5684  imaiun  6138  snnex  6588  unon  6649  opabex3d  6762  opabex3  6763  fparlem1  6884  fparlem2  6885  oarec  7248  ecid  7413  qsid  7414  mapval2  7486  ixpin  7532  onfin2  7747  unfilem1  7818  unifpw  7857  dfom5  8100  alephsuc2  8493  ackbij2  8655  isf33lem  8778  dffin7-2  8810  fin1a2lem6  8817  acncc  8852  fin41  8856  iunfo  8946  grutsk  9230  grothac  9238  grothtsk  9243  dfz2  10923  qexALT  11242  om2uzrani  12104  hashkf  12454  divalglem4  14263  1nprm  14431  nsgacs  16561  oppgsubm  16721  oppgsubg  16722  oppgcntz  16723  pmtrprfvalrn  16837  opprsubg  17605  opprunit  17630  opprirred  17671  opprsubrg  17770  00lss  17908  00ply1bas  18601  dfprm2  18831  unocv  19009  iunocv  19010  unisngl  20320  zcld  21610  iundisj  22250  plyun0  22886  aannenlem2  23017  eqid1  25592  choc0  26658  chocnul  26660  spanunsni  26911  lncnbd  27370  adjbd1o  27417  rnbra  27439  pjimai  27508  rabtru  27814  iunin1f  27853  iundisjf  27881  dfrp2  28029  xrdifh  28039  iundisjfi  28049  cmpcref  28306  eulerpartgbij  28817  eulerpartlemr  28819  dfdm5  29991  dfrn5  29992  dffix2  30243  fixcnv  30246  dfom5b  30250  fnimage  30267  brimg  30275  bj-vjust  30936  bj-csbsnlem  31034  bj-projun  31117  iundif1  31409  csbcom2fi  31816  csbgfi  31817  prtlem16  31892  aaitgo  35475  imaiun1  35630  nzss  36070  dfodd2  37719  dfeven5  37749  dfodd7  37750
  Copyright terms: Public domain W3C validator