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

Theorem eqriv 2802
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 2799 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1884 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637  wcel 2158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2798
This theorem is referenced by:  eqid  2805  cbvab  2929  vjust  3391  rabtru  3555  nfccdeq  3628  difeqri  3926  uneqri  3951  incom  4001  ineqri  4002  symdifass  4048  symdifassOLD  4049  indifdir  4082  undif3  4087  csbcom  4188  csbab  4203  pwpr  4620  pwtp  4621  pwv  4623  uniun  4647  int0  4679  intun  4697  intpr  4698  iuncom  4715  iuncom4  4716  iunin2  4772  iinun2  4774  iundif2  4775  iunun  4792  iunxun  4793  iunxiun  4796  iinpw  4805  inuni  5015  unipw  5105  xpiundi  5370  xpiundir  5371  iunxpf  5469  cnvuni  5507  dmiun  5531  dmuni  5532  idinxpres  5662  epini  5702  rniun  5751  xpdifid  5770  cnvresima  5834  imaco  5851  rnco  5852  dfmpt3  6222  imaiun  6724  snnexOLD  7194  unon  7258  opabex3d  7372  opabex3  7373  fparlem1  7508  fparlem2  7509  oarec  7876  ecid  8044  qsid  8045  mapval2  8119  ixpin  8167  onfin2  8388  unfilem1  8460  unifpw  8505  dfom5  8791  alephsuc2  9183  ackbij2  9347  isf33lem  9470  dffin7-2  9502  fin1a2lem6  9509  acncc  9544  fin41  9548  iunfo  9643  grutsk  9926  grothac  9934  grothtsk  9939  dfz2  11657  qexALT  12018  om2uzrani  12971  hashkf  13335  divalglem4  15335  1nprm  15606  nsgacs  17828  oppgsubm  17989  oppgsubg  17990  oppgcntz  17991  pmtrprfvalrn  18105  opprsubg  18834  opprunit  18859  opprirred  18900  opprsubrg  19001  00lss  19142  00ply1bas  19814  dfprm2  20046  unocv  20230  iunocv  20231  toprntopon  20939  unisngl  21540  zcld  22825  iundisj  23525  plyun0  24163  aannenlem2  24294  eqid1  27650  choc0  28510  chocnul  28512  spanunsni  28763  lncnbd  29222  adjbd1o  29269  rnbra  29291  pjimai  29360  iunin1f  29696  iundisjf  29724  dfrp2  29856  xrdifh  29866  iundisjfi  29879  cmpcref  30239  eulerpartgbij  30756  eulerpartlemr  30758  oddprm2  31055  dfdm5  31993  dfrn5  31994  imaindm  31999  dffix2  32330  fixcnv  32333  dfom5b  32337  fnimage  32354  brimg  32362  bj-vjust  33097  bj-csbsnlem  33203  bj-projun  33289  bj-vjust2  33322  finxp1o  33542  iundif1  33693  poimirlem26  33745  csbcom2fi  34241  csbgfi  34242  prtlem16  34645  aaitgo  38230  imaiun1  38440  nzss  39013  dfodd2  42121  dfeven5  42150  dfodd7  42151
  Copyright terms: Public domain W3C validator