Theorem eqriv 2758

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

Step	Hyp	Ref	Expression
1		dfcleq 2754	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1832	1 ⊢ 𝐴 = 𝐵

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  eqid  2761  cbvabv  2831  cbvabw  2832  cbvab  2833  vjust  3452  rabtru  3643  nfccdeq  3736  csbgfi  3867  difeqri  4076  uneqri  4103  ineqri  4158  symdifass  4208  indifdi  4240  undif3  4246  csbcom  4378  csbab  4398  pwpr  4861  pwtp  4862  pwv  4864  uniun  4890  int0  4922  intun  4940  iuncom  4959  iuncom4  4960  iunin2  5029  iinun2  5031  iundif2  5032  iunun  5053  iunxun  5054  iunxiun  5057  iinpw  5066  inuni  5311  unipw  5418  xpiundi  5722  xpiundir  5723  iunxpf  5826  cnvuni  5868  dmiun  5895  dmuni  5896  idinxpres  6041  rniun  6137  xpdifid  6158  xpdifcnvepel  6159  cnvresima  6224  imaco  6245  rnco  6246  rncoOLD  6247  imaindm  6295  dfmpt3  6665  imaiun  7241  unon  7831  opabex3d  7966  opabex3rd  7967  opabex3  7968  fparlem1  8112  fparlem2  8113  oarec  8554  ecid  8785  qsid  8786  mapval2  8884  ixpin  8935  onfin2  9216  unfilem1  9281  unifpw  9328  dfom5  9635  alephsuc2  10140  ackbij2  10301  isf33lem  10425  dffin7-2  10457  fin1a2lem6  10464  acncc  10499  fin41  10503  iunfo  10604  grutsk  10888  grothac  10896  grothtsk  10901  dfz2  12693  qexALT  13072  dfrp2  13506  om2uzrani  14075  hashkf  14456  divalglem4  16546  1nprm  16834  nsgacs  19352  oppgsubm  19556  oppgsubg  19557  oppgcntz  19558  pmtrprfvalrn  19682  opprsubg  20562  opprunit  20587  opprirred  20632  rimval  20710  dfric2  20737  opprsubrng  20791  opprsubrg  20825  00lss  21196  dfprm2  21759  unocv  21966  iunocv  21967  00ply1bas  22537  toprntopon  23223  unisngl  23826  zcld  25113  iundisj  25849  plyun0  26495  aannenlem2  26638  dfz12s2  28856  eqid1  31050  choc0  31910  chocnul  31912  spanunsni  32163  lncnbd  32622  adjbd1o  32669  rnbra  32691  pjimai  32760  iunin1f  33134  iundisjf  33165  xrdifh  33354  iundisjfi  33370  opprnsg  33990  0mplrim  34128  ccfldextdgrr  34286  cmpcref  34464  eulerpartgbij  34987  eulerpartlemr  34989  oddprm2  35267  dfdm5  36507  dfrn5  36508  dffix2  36637  fixcnv  36640  dfom5b  36644  fnimage  36661  brimg  36669  bj-csbsnlem  37785  bj-projun  37877  bj-pw0ALT  37932  bj-vjust  37938  finxp1o  38283  iundif1  38490  poimirlem26  38532  csbcom2fi  39028  dfsucmap3  39363  prtlem16  39894  sn-iotalem  43243  redvmptabs  43379  aaitgo  44122  imaiun1  44610  grumnueq  45230  nzss  45260  wrddin2  47842  chndin2  47847  chnrin2  47852  dfodd2  48678  dfeven5  48708  dfodd7  48709  dfidom2  49384  ixpv  49942  isoval2  50087  oppcciceq  50104  oppczeroo  50289  dfinito4  50553  lmdfval2  50707  cmdfval2  50708  initocmd  50721  termolmd  50722