Theorem eqriv 2619

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

Syntax hints:   ↔ wb 196   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqid  2622  cbvab  2746  vjust  3201  rabtru  3361  nfccdeq  3433  difeqri  3730  uneqri  3755  incom  3805  ineqri  3806  symdifass  3853  indifdir  3883  undif3  3888  undif3OLD  3889  csbcom  3994  csbab  4008  pwpr  4430  pwtp  4431  pwv  4433  uniun  4456  int0  4490  intun  4509  intpr  4510  iuncom  4527  iuncom4  4528  iunin2  4584  iinun2  4586  iundif2  4587  iunun  4604  iunxun  4605  iunxiun  4608  iinpw  4617  inuni  4826  unipw  4918  xpiundi  5173  xpiundir  5174  iunxpf  5270  cnvuni  5309  dmiun  5333  dmuni  5334  epini  5495  rniun  5543  xpdifid  5562  cnvresima  5623  imaco  5640  rnco  5641  dfmpt3  6014  imaiun  6503  snnexOLD  6967  unon  7031  opabex3d  7145  opabex3  7146  fparlem1  7277  fparlem2  7278  oarec  7642  ecid  7812  qsid  7813  mapval2  7887  ixpin  7933  onfin2  8152  unfilem1  8224  unifpw  8269  dfom5  8547  alephsuc2  8903  ackbij2  9065  isf33lem  9188  dffin7-2  9220  fin1a2lem6  9227  acncc  9262  fin41  9266  iunfo  9361  grutsk  9644  grothac  9652  grothtsk  9657  dfz2  11395  qexALT  11803  om2uzrani  12751  hashkf  13119  divalglem4  15119  1nprm  15392  nsgacs  17630  oppgsubm  17792  oppgsubg  17793  oppgcntz  17794  pmtrprfvalrn  17908  opprsubg  18636  opprunit  18661  opprirred  18702  opprsubrg  18801  00lss  18942  00ply1bas  19610  dfprm2  19842  unocv  20024  iunocv  20025  toprntopon  20729  unisngl  21330  zcld  22616  iundisj  23316  plyun0  23953  aannenlem2  24084  eqid1  27323  choc0  28185  chocnul  28187  spanunsni  28438  lncnbd  28897  adjbd1o  28944  rnbra  28966  pjimai  29035  iunin1f  29374  iundisjf  29402  dfrp2  29532  xrdifh  29542  iundisjfi  29555  cmpcref  29917  eulerpartgbij  30434  eulerpartlemr  30436  oddprm2  30733  dfdm5  31676  dfrn5  31677  imaindm  31682  dffix2  32012  fixcnv  32015  dfom5b  32019  fnimage  32036  brimg  32044  bj-vjust  32786  bj-csbsnlem  32898  bj-projun  32982  bj-vjust2  33015  finxp1o  33229  iundif1  33383  poimirlem26  33435  csbcom2fi  33934  csbgfi  33935  prtlem16  34154  aaitgo  37732  imaiun1  37943  nzss  38516  dfodd2  41549  dfeven5  41578  dfodd7  41579