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

Theorem eqriv 2618
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 2615 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1725 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1482  wcel 1989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-cleq 2614
This theorem is referenced by:  eqid  2621  cbvab  2745  vjust  3199  rabtru  3359  nfccdeq  3431  difeqri  3728  uneqri  3753  incom  3803  ineqri  3804  symdifass  3851  indifdir  3881  undif3  3886  undif3OLD  3887  csbcom  3992  csbab  4006  pwpr  4428  pwtp  4429  pwv  4431  uniun  4454  int0  4488  intun  4507  intpr  4508  iuncom  4525  iuncom4  4526  iunin2  4582  iinun2  4584  iundif2  4585  iunun  4602  iunxun  4603  iunxiun  4606  iinpw  4615  inuni  4824  unipw  4916  xpiundi  5171  xpiundir  5172  iunxpf  5268  cnvuni  5307  dmiun  5331  dmuni  5332  epini  5493  rniun  5541  xpdifid  5560  cnvresima  5621  imaco  5638  rnco  5639  dfmpt3  6012  imaiun  6500  snnexOLD  6964  unon  7028  opabex3d  7142  opabex3  7143  fparlem1  7274  fparlem2  7275  oarec  7639  ecid  7809  qsid  7810  mapval2  7884  ixpin  7930  onfin2  8149  unfilem1  8221  unifpw  8266  dfom5  8544  alephsuc2  8900  ackbij2  9062  isf33lem  9185  dffin7-2  9217  fin1a2lem6  9224  acncc  9259  fin41  9263  iunfo  9358  grutsk  9641  grothac  9649  grothtsk  9654  dfz2  11392  qexALT  11800  om2uzrani  12746  hashkf  13114  divalglem4  15113  1nprm  15386  nsgacs  17624  oppgsubm  17786  oppgsubg  17787  oppgcntz  17788  pmtrprfvalrn  17902  opprsubg  18630  opprunit  18655  opprirred  18696  opprsubrg  18795  00lss  18936  00ply1bas  19604  dfprm2  19836  unocv  20018  iunocv  20019  toprntopon  20723  unisngl  21324  zcld  22610  iundisj  23310  plyun0  23947  aannenlem2  24078  eqid1  27307  choc0  28169  chocnul  28171  spanunsni  28422  lncnbd  28881  adjbd1o  28928  rnbra  28950  pjimai  29019  iunin1f  29358  iundisjf  29386  dfrp2  29517  xrdifh  29527  iundisjfi  29540  cmpcref  29902  eulerpartgbij  30419  eulerpartlemr  30421  oddprm2  30718  dfdm5  31660  dfrn5  31661  imaindm  31666  dffix2  31996  fixcnv  31999  dfom5b  32003  fnimage  32020  brimg  32028  bj-vjust  32770  bj-csbsnlem  32882  bj-projun  32966  bj-vjust2  32999  finxp1o  33209  iundif1  33363  poimirlem26  33415  csbcom2fi  33914  csbgfi  33915  prtlem16  33980  aaitgo  37558  imaiun1  37769  nzss  38342  dfodd2  41320  dfeven5  41349  dfodd7  41350
  Copyright terms: Public domain W3C validator