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

Theorem eqriv 2463
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 2460 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1605 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  eqid  2467  cbvab  2608  cbvabOLD  2609  vjust  3114  nfccdeq  3329  difeqri  3624  uneqri  3646  incom  3691  ineqri  3692  indifdir  3754  undif3  3759  csbcom  3837  csbab  3855  pwpr  4241  pwtp  4242  pwv  4244  uniun  4264  intun  4314  intpr  4315  iuncom  4332  iuncom4  4333  iun0  4381  0iun  4382  iunin2  4389  iinun2  4391  iundif2  4392  iunun  4406  iunxun  4407  iunxiun  4408  iinpw  4414  inuni  4609  unipw  4697  xpiundi  5053  xpiundir  5054  0xp  5079  iunxpf  5150  cnvuni  5188  dmiun  5210  dmuni  5211  epini  5366  rniun  5415  xpdifid  5434  cnvresima  5495  imaco  5511  rnco  5512  dfmpt3  5702  imaiun  6144  snnex  6585  unon  6645  opabex3d  6762  opabex3  6763  fparlem1  6883  fparlem2  6884  oarec  7211  ecid  7376  qsid  7377  mapval2  7448  ixpin  7494  onfin2  7709  unfilem1  7783  unifpw  7822  dfom5  8066  alephsuc2  8460  ackbij2  8622  isf33lem  8745  dffin7-2  8777  fin1a2lem6  8784  acncc  8819  fin41  8823  iunfo  8913  grutsk  9199  grothac  9207  grothtsk  9212  dfz2  10881  qexALT  11196  om2uzrani  12030  hashkf  12374  divalglem4  13912  1nprm  14080  nsgacs  16039  oppgsubm  16199  oppgsubg  16200  oppgcntz  16201  pmtrprfvalrn  16316  opprsubg  17081  opprunit  17106  opprirred  17147  opprsubrg  17245  00lss  17383  00ply1bas  18068  dfprm2  18307  dfprm2OLD  18310  unocv  18494  iunocv  18495  zcld  21069  iundisj  21709  plyun0  22345  aannenlem2  22475  eqid1  24867  choc0  25936  chocnul  25938  spanunsni  26189  lncnbd  26649  adjbd1o  26696  rnbra  26718  pjimai  26787  iundisjf  27137  xrdifh  27275  iundisjfi  27285  eulerpartgbij  27967  eulerpartlemr  27969  dfdm5  28799  dfrn5  28800  symdifass  29070  dffix2  29148  fixcnv  29151  dfom5b  29155  fnimage  29172  brimg  29180  iundif1  29630  csbcom2fi  30154  csbgfi  30155  prtlem16  30230  aaitgo  30732  nzss  30838  bj-vjust  33462  bj-csbsnlem  33560  bj-projun  33642
  Copyright terms: Public domain W3C validator