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

Theorem eqriv 2648
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 2645 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1766 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  eqid  2651  cbvab  2775  vjust  3232  rabtru  3393  nfccdeq  3466  difeqri  3763  uneqri  3788  incom  3838  ineqri  3839  symdifass  3886  indifdir  3916  undif3  3921  undif3OLD  3922  csbcom  4027  csbab  4041  pwpr  4462  pwtp  4463  pwv  4465  uniun  4488  int0  4522  intun  4541  intpr  4542  iuncom  4559  iuncom4  4560  iunin2  4616  iinun2  4618  iundif2  4619  iunun  4636  iunxun  4637  iunxiun  4640  iinpw  4649  inuni  4856  unipw  4948  xpiundi  5207  xpiundir  5208  iunxpf  5303  cnvuni  5341  dmiun  5365  dmuni  5366  epini  5530  rniun  5578  xpdifid  5597  cnvresima  5661  imaco  5678  rnco  5679  dfmpt3  6052  imaiun  6543  snnexOLD  7009  unon  7073  opabex3d  7187  opabex3  7188  fparlem1  7322  fparlem2  7323  oarec  7687  ecid  7855  qsid  7856  mapval2  7929  ixpin  7975  onfin2  8193  unfilem1  8265  unifpw  8310  dfom5  8585  alephsuc2  8941  ackbij2  9103  isf33lem  9226  dffin7-2  9258  fin1a2lem6  9265  acncc  9300  fin41  9304  iunfo  9399  grutsk  9682  grothac  9690  grothtsk  9695  dfz2  11433  qexALT  11841  om2uzrani  12791  hashkf  13159  divalglem4  15166  1nprm  15439  nsgacs  17677  oppgsubm  17838  oppgsubg  17839  oppgcntz  17840  pmtrprfvalrn  17954  opprsubg  18682  opprunit  18707  opprirred  18748  opprsubrg  18849  00lss  18990  00ply1bas  19658  dfprm2  19890  unocv  20072  iunocv  20073  toprntopon  20777  unisngl  21378  zcld  22663  iundisj  23362  plyun0  23998  aannenlem2  24129  eqid1  27453  choc0  28313  chocnul  28315  spanunsni  28566  lncnbd  29025  adjbd1o  29072  rnbra  29094  pjimai  29163  iunin1f  29500  iundisjf  29528  dfrp2  29660  xrdifh  29670  iundisjfi  29683  cmpcref  30045  eulerpartgbij  30562  eulerpartlemr  30564  oddprm2  30861  dfdm5  31800  dfrn5  31801  imaindm  31806  dffix2  32137  fixcnv  32140  dfom5b  32144  fnimage  32161  brimg  32169  bj-vjust  32911  bj-csbsnlem  33023  bj-projun  33107  bj-vjust2  33140  finxp1o  33359  iundif1  33513  poimirlem26  33565  csbcom2fi  34064  csbgfi  34065  prtlem16  34473  aaitgo  38049  imaiun1  38260  nzss  38833  dfodd2  41874  dfeven5  41903  dfodd7  41904
  Copyright terms: Public domain W3C validator