Theorem eqriv 2792

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

Syntax hints:   ↔ wb 207   = wceq 1522   ∈ wcel 2081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788

This theorem is referenced by:  eqid  2795  cbvabv  2927  cbvab  2928  vjust  3438  rabtru  3616  nfccdeq  3706  csbgfi  3833  difeqri  4026  uneqri  4052  incom  4103  ineqri  4104  symdifass  4152  indifdir  4184  undif3  4189  csbcom  4293  csbab  4308  pwpr  4743  pwtp  4744  pwv  4746  uniun  4768  int0  4800  intun  4818  intpr  4819  iuncom  4836  iuncom4  4837  iunin2  4896  iinun2  4898  iundif2  4899  iunun  4918  iunxun  4919  iunxiun  4922  iinpw  4931  inuni  5142  unipw  5239  xpiundi  5513  xpiundir  5514  iunxpf  5610  cnvuni  5648  dmiun  5673  dmuni  5674  idinxpres  5800  epini  5840  rniun  5887  xpdifid  5906  cnvresima  5967  imaco  5984  rnco  5985  dfmpt3  6355  imaiun  6874  unon  7407  opabex3d  7527  opabex3rd  7528  opabex3  7529  fparlem1  7668  fparlem2  7669  oarec  8043  ecid  8217  qsid  8218  mapval2  8291  ixpin  8340  onfin2  8561  unfilem1  8633  unifpw  8678  dfom5  8964  alephsuc2  9357  ackbij2  9516  isf33lem  9639  dffin7-2  9671  fin1a2lem6  9678  acncc  9713  fin41  9717  iunfo  9812  grutsk  10095  grothac  10103  grothtsk  10108  dfz2  11853  qexALT  12218  om2uzrani  13175  hashkf  13547  divalglem4  15585  1nprm  15857  nsgacs  18074  oppgsubm  18236  oppgsubg  18237  oppgcntz  18238  pmtrprfvalrn  18352  opprsubg  19081  opprunit  19106  opprirred  19147  opprsubrg  19251  00lss  19408  00ply1bas  20096  dfprm2  20328  unocv  20511  iunocv  20512  toprntopon  21222  unisngl  21824  zcld  23109  iundisj  23837  plyun0  24475  aannenlem2  24606  eqid1  27942  choc0  28799  chocnul  28801  spanunsni  29052  lncnbd  29511  adjbd1o  29558  rnbra  29580  pjimai  29649  iunin1f  30004  iundisjf  30034  dfrp2  30184  xrdifh  30196  iundisjfi  30210  ccfldextdgrr  30666  cmpcref  30736  eulerpartgbij  31252  eulerpartlemr  31254  oddprm2  31548  dfdm5  32631  dfrn5  32632  imaindm  32637  dffix2  32982  fixcnv  32985  dfom5b  32989  fnimage  33006  brimg  33014  bj-csbsnlem  33802  bj-projun  33937  bj-vjust  33970  finxp1o  34230  wl-dfrabv  34419  iundif1  34423  poimirlem26  34475  csbcom2fi  34964  prtlem16  35562  aaitgo  39273  imaiun1  39507  grumnueq  40146  nzss  40213  dfodd2  43310  dfeven5  43340  dfodd7  43341