Theorem eqriv 2759

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 2755	. 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 2734

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

This theorem is used by:  eqid  2762  cbvabv  2832  cbvabw  2833  cbvab  2834  vjust  3454  rabtru  3646  nfccdeq  3739  csbgfi  3870  difeqri  4079  uneqri  4106  ineqri  4161  symdifass  4211  indifdi  4243  undif3  4249  csbcom  4381  csbab  4401  pwpr  4864  pwtp  4865  pwv  4867  uniun  4893  int0  4925  intun  4943  iuncom  4962  iuncom4  4963  iunin2  5033  iinun2  5035  iundif2  5036  iunun  5057  iunxun  5058  iunxiun  5061  iinpw  5070  inuni  5318  unipw  5429  xpiundi  5730  xpiundir  5731  iunxpf  5832  cnvuni  5874  dmiun  5901  dmuni  5902  idinxpres  6047  rniun  6143  xpdifid  6164  xpdifcnvepel  6165  cnvresima  6230  imaco  6251  rnco  6252  rncoOLD  6253  imaindm  6301  dfmpt3  6670  imaiun  7246  unon  7831  opabex3d  7966  opabex3rd  7967  opabex3  7968  fparlem1  8113  fparlem2  8114  oarec  8553  ecid  8784  qsid  8785  mapval2  8883  ixpin  8934  onfin2  9215  unfilem1  9279  unifpw  9326  dfom5  9633  alephsuc2  10087  ackbij2  10248  isf33lem  10372  dffin7-2  10404  fin1a2lem6  10411  acncc  10446  fin41  10450  iunfo  10551  grutsk  10835  grothac  10843  grothtsk  10848  dfz2  12638  qexALT  13017  dfrp2  13451  om2uzrani  14020  hashkf  14400  divalglem4  16492  1nprm  16775  nsgacs  19291  oppgsubm  19495  oppgsubg  19496  oppgcntz  19497  pmtrprfvalrn  19621  opprsubg  20499  opprunit  20524  opprirred  20569  rimval  20647  opprsubrng  20727  opprsubrg  20761  00lss  21131  dfprm2  21692  unocv  21899  iunocv  21900  00ply1bas  22470  toprntopon  23156  unisngl  23759  zcld  25046  iundisj  25782  plyun0  26429  aannenlem2  26572  dfz12s2  28761  eqid1  30955  choc0  31815  chocnul  31817  spanunsni  32068  lncnbd  32527  adjbd1o  32574  rnbra  32596  pjimai  32665  iunin1f  33039  iundisjf  33070  xrdifh  33259  iundisjfi  33275  opprnsg  33894  0mplrim  34032  ccfldextdgrr  34190  cmpcref  34368  eulerpartgbij  34891  eulerpartlemr  34893  oddprm2  35171  dfdm5  36360  dfrn5  36361  dffix2  36490  fixcnv  36493  dfom5b  36497  fnimage  36514  brimg  36522  bj-csbsnlem  37654  bj-projun  37746  bj-pw0ALT  37801  bj-vjust  37807  finxp1o  38154  iundif1  38361  poimirlem26  38403  csbcom2fi  38884  dfsucmap3  39219  prtlem16  39750  sn-iotalem  43099  redvmptabs  43243  aaitgo  44011  imaiun1  44499  grumnueq  45119  nzss  45149  wrddin2  47724  chndin2  47729  chnrin2  47734  dfodd2  48560  dfeven5  48590  dfodd7  48591  dfidom2  49266  ixpv  49824  isoval2  49969  oppcciceq  49986  oppczeroo  50171  dfinito4  50435  lmdfval2  50589  cmdfval2  50590  initocmd  50603  termolmd  50604