Theorem eqriv 2763

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 2759	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1832	1 ⊢ 𝐴 = 𝐵

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

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 2156  ax-ext 2738

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

This theorem is used by:  eqid  2766  cbvabv  2836  cbvabw  2837  cbvab  2838  vjust  3459  rabtru  3651  nfccdeq  3744  csbgfi  3876  difeqri  4086  uneqri  4113  ineqri  4168  symdifass  4218  indifdi  4250  undif3  4256  csbcom  4388  csbab  4408  pwpr  4871  pwtp  4872  pwv  4874  uniun  4900  int0  4932  intun  4950  iuncom  4969  iuncom4  4970  iunin2  5040  iinun2  5042  iundif2  5043  iunun  5064  iunxun  5065  iunxiun  5068  iinpw  5077  inuni  5325  unipw  5436  xpiundi  5737  xpiundir  5738  iunxpf  5839  cnvuni  5881  dmiun  5908  dmuni  5909  idinxpres  6054  rniun  6150  xpdifid  6170  xpdifcnvepel  6171  cnvresima  6236  imaco  6257  rnco  6258  rncoOLD  6259  imaindm  6307  dfmpt3  6676  imaiun  7250  unon  7836  opabex3d  7971  opabex3rd  7972  opabex3  7973  fparlem1  8116  fparlem2  8117  oarec  8556  ecid  8787  qsid  8788  mapval2  8879  ixpin  8930  onfin2  9211  unfilem1  9275  unifpw  9322  dfom5  9629  alephsuc2  10083  ackbij2  10244  isf33lem  10368  dffin7-2  10400  fin1a2lem6  10407  acncc  10442  fin41  10446  iunfo  10541  grutsk  10825  grothac  10833  grothtsk  10838  dfz2  12628  qexALT  13006  dfrp2  13439  om2uzrani  14008  hashkf  14388  divalglem4  16479  1nprm  16762  nsgacs  19259  oppgsubm  19463  oppgsubg  19464  oppgcntz  19465  pmtrprfvalrn  19589  opprsubg  20467  opprunit  20492  opprirred  20537  rimval  20615  opprsubrng  20695  opprsubrg  20729  00lss  21099  dfprm2  21660  unocv  21867  iunocv  21868  00ply1bas  22436  toprntopon  23119  unisngl  23721  zcld  25008  iundisj  25744  plyun0  26391  aannenlem2  26529  dfz12s2  28718  eqid1  30855  choc0  31715  chocnul  31717  spanunsni  31968  lncnbd  32427  adjbd1o  32474  rnbra  32496  pjimai  32565  iunin1f  32939  iundisjf  32971  xrdifh  33162  iundisjfi  33178  opprnsg  33797  0mplrim  33935  ccfldextdgrr  34093  cmpcref  34271  eulerpartgbij  34794  eulerpartlemr  34796  oddprm2  35074  dfdm5  36286  dfrn5  36287  dffix2  36416  fixcnv  36419  dfom5b  36423  fnimage  36440  brimg  36448  bj-csbsnlem  37579  bj-projun  37671  bj-pw0ALT  37726  bj-vjust  37732  finxp1o  38079  iundif1  38286  poimirlem26  38338  csbcom2fi  38818  dfsucmap3  39153  prtlem16  39684  sn-iotalem  43033  redvmptabs  43162  aaitgo  43930  imaiun1  44418  grumnueq  45038  nzss  45068  dfodd2  48442  dfeven5  48472  dfodd7  48473  dfidom2  49149  ixpv  49709  isoval2  49854  oppcciceq  49871  oppczeroo  50056  dfinito4  50320  lmdfval2  50474  cmdfval2  50475  initocmd  50488  termolmd  50489