Theorem eqriv 2760

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqid  2763  cbvabv  2834  cbvabw  2835  cbvab  2836  vjust  3455  rabtru  3646  nfccdeq  3739  csbgfi  3871  difeqri  4068  ineqri  4112  uneqri  4158  symdifass  4210  indifdi  4242  undif3  4248  csbcom  4381  csbab  4401  pwv  4578  pwpr  4831  pwtp  4832  uniun  4893  int0  4925  intun  4943  iuncom  4962  iuncom4  4963  iunin2  5032  iinun2  5034  iundif2  5035  iunun  5056  iunxun  5057  iunxiun  5060  iinpw  5069  inuni  5316  unipw  5423  xpiundi  5727  xpiundir  5728  iunxpf  5833  cnvuni  5876  dmiun  5903  dmuni  5904  idinxpres  6052  rniun  6152  xpdifid  6172  xpdifcnvepel  6173  cnvresima  6245  imaco  6266  rnco  6267  rncoOLD  6268  imaindm  6323  dfmpt3  6698  imaiun  7275  unon  7869  opabex3d  8004  opabex3rd  8005  opabex3  8006  fparlem1  8153  fparlem2  8154  oarec  8601  ecid  8832  qsid  8833  mapval2  8931  ixpin  8982  onfin2  9263  unfilem1  9328  unifpw  9375  dfom5  9681  alephsuc2  10189  ackbij2  10350  isf33lem  10474  dffin7-2  10506  fin1a2lem6  10513  acncc  10548  fin41  10552  iunfo  10653  grutsk  10937  grothac  10945  grothtsk  10950  dfz2  12742  qexALT  13121  dfrp2  13555  om2uzrani  14125  hashkf  14506  divalglem4  16598  1nprm  16886  nsgacs  19404  oppgsubm  19609  oppgsubg  19610  oppgcntz  19611  pmtrprfvalrn  19735  opprsubg  20615  opprunit  20640  opprirred  20685  rimval  20763  dfric2  20790  opprsubrng  20844  opprsubrg  20878  00lss  21249  dfprm2  21812  unocv  22019  iunocv  22020  00ply1bas  22590  toprntopon  23276  unisngl  23879  zcld  25166  iundisj  25902  plyun0  26548  aannenlem2  26689  dfz12s2  28907  eqid1  31101  choc0  31961  chocnul  31963  spanunsni  32214  lncnbd  32673  adjbd1o  32720  rnbra  32742  pjimai  32811  iunin1f  33227  iundisjf  33258  xrdifh  33445  iundisjfi  33461  opprnsg  34092  0mplrim  34229  ccfldextdgrr  34387  cmpcref  34565  eulerpartgbij  35087  eulerpartlemr  35089  oddprm2  35367  dfdm5  36728  dfrn5  36729  dffix2  36858  fixcnv  36861  dfom5b  36865  fnimage  36882  brimg  36890  bj-csbsnlem  38006  bj-projun  38098  bj-dfres2  38154  bj-pw0ALT  38168  bj-vjust  38174  finxp1o  38520  iundif1  38727  poimirlem26  38769  csbcom2fi  39263  dfsucmap3  39598  prtlem16  40129  sn-iotalem  43479  redvmptabs  43615  aaitgo  44367  imaiun1  44854  grumnueq  45474  nzss  45504  wrddin2  48113  chndin2  48118  chnrin2  48123  dfodd2  48949  dfeven5  48979  dfodd7  48980  dfidom2  49655  ixpv  50218  isoval2  50364  oppcciceq  50381  oppczeroo  50574  dfinito4  50851  lmdfval2  51053  cmdfval2  51054  initocmd  51067  termolmd  51068