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

Theorem eqriv 2419
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 2416 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1670 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    = wceq 1438    e. wcel 1869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-cleq 2415
This theorem is referenced by:  eqid  2423  cbvab  2564  cbvabOLD  2565  vjust  3083  nfccdeq  3298  difeqri  3586  uneqri  3609  incom  3656  ineqri  3657  symdifass  3703  indifdir  3730  undif3  3735  csbcom  3812  csbab  3826  pwpr  4213  pwtp  4214  pwv  4216  uniun  4236  intun  4286  intpr  4287  iuncom  4304  iuncom4  4305  iun0  4353  0iun  4354  iunin2  4361  iinun2  4363  iundif2  4364  iunun  4381  iunxun  4382  iunxiun  4383  iinpw  4389  inuni  4584  unipw  4669  xpiundi  4906  xpiundir  4907  0xp  4932  iunxpf  5000  cnvuni  5038  dmiun  5060  dmuni  5061  epini  5215  rniun  5263  xpdifid  5282  cnvresima  5341  imaco  5357  rnco  5358  dfmpt3  5714  imaiun  6163  snnex  6609  unon  6670  opabex3d  6783  opabex3  6784  fparlem1  6905  fparlem2  6906  oarec  7269  ecid  7434  qsid  7435  mapval2  7507  ixpin  7553  onfin2  7768  unfilem1  7839  unifpw  7881  dfom5  8159  alephsuc2  8513  ackbij2  8675  isf33lem  8798  dffin7-2  8830  fin1a2lem6  8837  acncc  8872  fin41  8876  iunfo  8966  grutsk  9249  grothac  9257  grothtsk  9262  dfz2  10957  qexALT  11281  om2uzrani  12167  hashkf  12518  divalglem4  14368  1nprm  14622  nsgacs  16846  oppgsubm  17006  oppgsubg  17007  oppgcntz  17008  pmtrprfvalrn  17122  opprsubg  17857  opprunit  17882  opprirred  17923  opprsubrg  18022  00lss  18158  00ply1bas  18826  dfprm2  19057  unocv  19235  iunocv  19236  unisngl  20534  zcld  21823  iundisj  22493  plyun0  23143  aannenlem2  23277  eqid1  25896  choc0  26971  chocnul  26973  spanunsni  27224  lncnbd  27683  adjbd1o  27730  rnbra  27752  pjimai  27821  rabtru  28128  iunin1f  28167  iundisjf  28195  dfrp2  28352  xrdifh  28362  iundisjfi  28372  cmpcref  28679  eulerpartgbij  29207  eulerpartlemr  29209  dfdm5  30419  dfrn5  30420  dffix2  30671  fixcnv  30674  dfom5b  30678  fnimage  30695  brimg  30703  bj-vjust  31365  bj-csbsnlem  31468  bj-projun  31550  finxp0  31741  finxp1o  31742  iundif1  31885  poimirlem26  31924  csbcom2fi  32327  csbgfi  32328  prtlem16  32403  aaitgo  35992  imaiun1  36147  nzss  36568  dfodd2  38522  dfeven5  38552  dfodd7  38553
  Copyright terms: Public domain W3C validator