Theorem eqriv 2728

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqid  2731  cbvabv  2801  cbvabw  2802  cbvab  2803  vjust  3437  rabtru  3645  nfccdeq  3737  csbgfi  3870  difeqri  4078  uneqri  4106  ineqri  4162  symdifass  4212  indifdi  4244  undif3  4250  csbcom  4370  csbab  4390  pwpr  4853  pwtp  4854  pwv  4856  uniun  4882  int0  4912  intun  4930  iuncom  4949  iuncom4  4950  iunin2  5019  iinun2  5021  iundif2  5022  iunun  5041  iunxun  5042  iunxiun  5045  iinpw  5054  inuni  5288  unipw  5391  xpiundi  5687  xpiundir  5688  iunxpf  5788  cnvuni  5826  dmiun  5853  dmuni  5854  idinxpres  5996  rniun  6094  xpdifid  6115  cnvresima  6177  imaco  6198  rnco  6199  rncoOLD  6200  imaindm  6246  dfmpt3  6615  imaiun  7179  unon  7761  opabex3d  7897  opabex3rd  7898  opabex3  7899  fparlem1  8042  fparlem2  8043  oarec  8477  ecid  8704  qsid  8705  mapval2  8796  ixpin  8847  onfin2  9125  unfilem1  9189  unifpw  9239  dfom5  9540  alephsuc2  9968  ackbij2  10130  isf33lem  10254  dffin7-2  10286  fin1a2lem6  10293  acncc  10328  fin41  10332  iunfo  10427  grutsk  10710  grothac  10718  grothtsk  10723  dfz2  12484  qexALT  12859  dfrp2  13291  om2uzrani  13856  hashkf  14236  divalglem4  16304  1nprm  16587  nsgacs  19072  oppgsubm  19272  oppgsubg  19273  oppgcntz  19274  pmtrprfvalrn  19398  opprsubg  20268  opprunit  20293  opprirred  20338  opprsubrng  20472  opprsubrg  20506  00lss  20872  dfprm2  21408  unocv  21615  iunocv  21616  00ply1bas  22150  toprntopon  22838  unisngl  23440  zcld  24727  iundisj  25474  plyun0  26127  aannenlem2  26262  eqid1  30442  choc0  31301  chocnul  31303  spanunsni  31554  lncnbd  32013  adjbd1o  32060  rnbra  32082  pjimai  32151  iunin1f  32532  iundisjf  32564  xrdifh  32758  iundisjfi  32773  opprnsg  33444  ccfldextdgrr  33680  cmpcref  33858  eulerpartgbij  34380  eulerpartlemr  34382  oddprm2  34663  dfdm5  35805  dfrn5  35806  dffix2  35938  fixcnv  35941  dfom5b  35945  fnimage  35962  brimg  35970  bj-csbsnlem  36936  bj-projun  37027  bj-pw0ALT  37082  bj-vjust  37088  finxp1o  37425  iundif1  37633  poimirlem26  37685  csbcom2fi  38167  prtlem16  38907  sn-iotalem  42253  redvmptabs  42392  aaitgo  43194  imaiun1  43683  grumnueq  44319  nzss  44349  dfodd2  47666  dfeven5  47696  dfodd7  47697  ixpv  48920  isoval2  49066  oppcciceq  49083  oppczeroo  49268  dfinito4  49532  lmdfval2  49686  cmdfval2  49687  initocmd  49700  termolmd  49701