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

Theorem eqriv 2606
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 2603 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1716 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  eqid  2609  cbvab  2732  vjust  3173  nfccdeq  3399  difeqri  3691  uneqri  3716  incom  3766  ineqri  3767  symdifass  3814  indifdir  3841  undif3  3846  undif3OLD  3847  csbcom  3945  csbab  3959  pwpr  4362  pwtp  4363  pwv  4365  uniun  4386  int0  4419  intun  4438  intpr  4439  iuncom  4457  iuncom4  4458  iun0  4506  0iun  4507  iunin2  4514  iinun2  4516  iundif2  4517  iunun  4534  iunxun  4535  iunxiun  4538  iinpw  4544  inuni  4747  unipw  4838  xpiundi  5085  xpiundir  5086  0xp  5111  iunxpf  5179  cnvuni  5218  dmiun  5241  dmuni  5242  epini  5400  rniun  5447  xpdifid  5466  cnvresima  5526  imaco  5542  rnco  5543  dfmpt3  5912  imaiun  6384  snnex  6839  unon  6900  opabex3d  7014  opabex3  7015  fparlem1  7141  fparlem2  7142  oarec  7506  ecid  7676  qsid  7677  mapval2  7750  ixpin  7796  onfin2  8014  unfilem1  8086  unifpw  8129  dfom5  8407  alephsuc2  8763  ackbij2  8925  isf33lem  9048  dffin7-2  9080  fin1a2lem6  9087  acncc  9122  fin41  9126  iunfo  9217  grutsk  9500  grothac  9508  grothtsk  9513  dfz2  11230  qexALT  11637  om2uzrani  12570  hashkf  12938  divalglem4  14905  1nprm  15178  nsgacs  17401  oppgsubm  17563  oppgsubg  17564  oppgcntz  17565  pmtrprfvalrn  17679  opprsubg  18407  opprunit  18432  opprirred  18473  opprsubrg  18572  00lss  18711  00ply1bas  19379  dfprm2  19608  unocv  19790  iunocv  19791  unisngl  21087  zcld  22371  iundisj  23067  plyun0  23701  aannenlem2  23832  eqid1  26508  choc0  27362  chocnul  27364  spanunsni  27615  lncnbd  28074  adjbd1o  28121  rnbra  28143  pjimai  28212  rabtru  28516  iunin1f  28550  iundisjf  28577  dfrp2  28715  xrdifh  28725  iundisjfi  28735  cmpcref  29038  eulerpartgbij  29554  eulerpartlemr  29556  dfdm5  30714  dfrn5  30715  dffix2  30975  fixcnv  30978  dfom5b  30982  fnimage  30999  brimg  31007  bj-vjust  31767  bj-csbsnlem  31873  bj-projun  31958  bj-vjust2  31989  bj-toprntopon  32027  finxp0  32187  finxp1o  32188  iundif1  32336  poimirlem26  32388  csbcom2fi  32887  csbgfi  32888  prtlem16  32955  aaitgo  36534  imaiun1  36745  nzss  37321  dfodd2  39871  dfeven5  39900  dfodd7  39901
  Copyright terms: Public domain W3C validator