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

Theorem eqriv 2607
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
eqriv.1 (𝑥𝐴𝑥𝐵)
Assertion
Ref Expression
eqriv 𝐴 = 𝐵
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eqriv
StepHypRef Expression
1 dfcleq 2604 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1717 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-cleq 2603
This theorem is referenced by:  eqid  2610  cbvab  2733  vjust  3174  nfccdeq  3400  difeqri  3692  uneqri  3717  incom  3767  ineqri  3768  symdifass  3815  indifdir  3842  undif3  3847  undif3OLD  3848  csbcom  3946  csbab  3960  pwpr  4368  pwtp  4369  pwv  4371  uniun  4392  int0  4425  intun  4444  intpr  4445  iuncom  4463  iuncom4  4464  iun0  4512  0iun  4513  iunin2  4520  iinun2  4522  iundif2  4523  iunun  4540  iunxun  4541  iunxiun  4544  iinpw  4550  inuni  4753  unipw  4845  xpiundi  5096  xpiundir  5097  0xp  5122  iunxpf  5192  cnvuni  5231  dmiun  5255  dmuni  5256  epini  5414  rniun  5462  xpdifid  5481  cnvresima  5541  imaco  5557  rnco  5558  dfmpt3  5927  imaiun  6407  snnex  6862  unon  6923  opabex3d  7037  opabex3  7038  fparlem1  7164  fparlem2  7165  oarec  7529  ecid  7699  qsid  7700  mapval2  7773  ixpin  7819  onfin2  8037  unfilem1  8109  unifpw  8152  dfom5  8430  alephsuc2  8786  ackbij2  8948  isf33lem  9071  dffin7-2  9103  fin1a2lem6  9110  acncc  9145  fin41  9149  iunfo  9240  grutsk  9523  grothac  9531  grothtsk  9536  dfz2  11272  qexALT  11679  om2uzrani  12613  hashkf  12981  divalglem4  14957  1nprm  15230  nsgacs  17453  oppgsubm  17615  oppgsubg  17616  oppgcntz  17617  pmtrprfvalrn  17731  opprsubg  18459  opprunit  18484  opprirred  18525  opprsubrg  18624  00lss  18763  00ply1bas  19431  dfprm2  19661  unocv  19843  iunocv  19844  unisngl  21140  zcld  22424  iundisj  23123  plyun0  23757  aannenlem2  23888  eqid1  26715  choc0  27569  chocnul  27571  spanunsni  27822  lncnbd  28281  adjbd1o  28328  rnbra  28350  pjimai  28419  rabtru  28723  iunin1f  28757  iundisjf  28784  dfrp2  28922  xrdifh  28932  iundisjfi  28942  cmpcref  29245  eulerpartgbij  29761  eulerpartlemr  29763  dfdm5  30921  dfrn5  30922  dffix2  31182  fixcnv  31185  dfom5b  31189  fnimage  31206  brimg  31214  bj-vjust  31974  bj-csbsnlem  32090  bj-projun  32175  bj-vjust2  32206  bj-toprntopon  32244  finxp0  32404  finxp1o  32405  iundif1  32553  poimirlem26  32605  csbcom2fi  33104  csbgfi  33105  prtlem16  33172  aaitgo  36751  imaiun1  36962  nzss  37538  dfodd2  40087  dfeven5  40116  dfodd7  40117
  Copyright terms: Public domain W3C validator