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

Theorem eqriv 2767
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 2764 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1873 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1630  wcel 2144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852  df-cleq 2763
This theorem is referenced by:  eqid  2770  cbvab  2894  vjust  3350  rabtru  3510  nfccdeq  3583  difeqri  3879  uneqri  3904  incom  3954  ineqri  3955  symdifass  4000  indifdir  4030  undif3  4035  csbcom  4136  csbab  4150  pwpr  4566  pwtp  4567  pwv  4569  uniun  4591  int0  4623  intun  4641  intpr  4642  iuncom  4659  iuncom4  4660  iunin2  4716  iinun2  4718  iundif2  4719  iunun  4736  iunxun  4737  iunxiun  4740  iinpw  4749  inuni  4954  unipw  5046  xpiundi  5313  xpiundir  5314  iunxpf  5409  cnvuni  5447  dmiun  5471  dmuni  5472  epini  5636  rniun  5684  xpdifid  5703  cnvresima  5767  imaco  5784  rnco  5785  dfmpt3  6154  imaiun  6645  snnexOLD  7113  unon  7177  opabex3d  7291  opabex3  7292  fparlem1  7427  fparlem2  7428  oarec  7795  ecid  7963  qsid  7964  mapval2  8038  ixpin  8086  onfin2  8307  unfilem1  8379  unifpw  8424  dfom5  8710  alephsuc2  9102  ackbij2  9266  isf33lem  9389  dffin7-2  9421  fin1a2lem6  9428  acncc  9463  fin41  9467  iunfo  9562  grutsk  9845  grothac  9853  grothtsk  9858  dfz2  11596  qexALT  12005  om2uzrani  12958  hashkf  13322  divalglem4  15326  1nprm  15598  nsgacs  17837  oppgsubm  17998  oppgsubg  17999  oppgcntz  18000  pmtrprfvalrn  18114  opprsubg  18843  opprunit  18868  opprirred  18909  opprsubrg  19010  00lss  19151  00ply1bas  19824  dfprm2  20056  unocv  20240  iunocv  20241  toprntopon  20949  unisngl  21550  zcld  22835  iundisj  23535  plyun0  24172  aannenlem2  24303  eqid1  27659  choc0  28519  chocnul  28521  spanunsni  28772  lncnbd  29231  adjbd1o  29278  rnbra  29300  pjimai  29369  iunin1f  29706  iundisjf  29734  dfrp2  29866  xrdifh  29876  iundisjfi  29889  cmpcref  30251  eulerpartgbij  30768  eulerpartlemr  30770  oddprm2  31067  dfdm5  32006  dfrn5  32007  imaindm  32012  dffix2  32343  fixcnv  32346  dfom5b  32350  fnimage  32367  brimg  32375  bj-vjust  33116  bj-csbsnlem  33221  bj-projun  33307  bj-vjust2  33340  finxp1o  33559  iundif1  33709  poimirlem26  33761  csbcom2fi  34259  csbgfi  34260  prtlem16  34670  aaitgo  38251  imaiun1  38462  nzss  39035  dfodd2  42067  dfeven5  42096  dfodd7  42097
  Copyright terms: Public domain W3C validator