Theorem eqriv 2735

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqid  2738  cbvabv  2812  cbvabw  2813  cbvabwOLD  2814  cbvab  2815  vjust  3423  rabtru  3614  nfccdeq  3708  csbgfi  3849  difeqri  4055  uneqri  4081  incomOLD  4132  ineqri  4135  symdifass  4182  indifdi  4214  indifdirOLD  4216  undif3  4221  csbcom  4348  csbab  4368  dfopif  4797  pwpr  4830  pwtp  4831  pwv  4833  uniun  4861  int0  4890  intun  4908  intprOLD  4911  iuncom  4928  iuncom4  4929  iunin2  4996  iinun2  4998  iundif2  4999  iunun  5018  iunxun  5019  iunxiun  5022  iinpw  5031  inuni  5262  unipw  5360  xpiundi  5648  xpiundir  5649  iunxpf  5746  cnvuni  5784  dmiun  5811  dmuni  5812  idinxpres  5943  rniun  6040  xpdifid  6060  cnvresima  6122  imaco  6144  rnco  6145  dfmpt3  6551  imaiun  7100  unon  7653  opabex3d  7781  opabex3rd  7782  opabex3  7783  fparlem1  7923  fparlem2  7924  oarec  8355  ecid  8529  qsid  8530  mapval2  8618  ixpin  8669  onfin2  8945  unfilem1  9008  unifpw  9052  dfom5  9338  alephsuc2  9767  ackbij2  9930  isf33lem  10053  dffin7-2  10085  fin1a2lem6  10092  acncc  10127  fin41  10131  iunfo  10226  grutsk  10509  grothac  10517  grothtsk  10522  dfz2  12268  qexALT  12633  dfrp2  13057  om2uzrani  13600  hashkf  13974  divalglem4  16033  1nprm  16312  nsgacs  18705  oppgsubm  18884  oppgsubg  18885  oppgcntz  18886  pmtrprfvalrn  19011  opprsubg  19793  opprunit  19818  opprirred  19859  opprsubrg  19960  00lss  20118  dfprm2  20607  unocv  20797  iunocv  20798  00ply1bas  21321  toprntopon  21982  unisngl  22586  zcld  23882  iundisj  24617  plyun0  25263  aannenlem2  25394  eqid1  28732  choc0  29589  chocnul  29591  spanunsni  29842  lncnbd  30301  adjbd1o  30348  rnbra  30370  pjimai  30439  iunin1f  30798  iundisjf  30829  xrdifh  31003  iundisjfi  31019  ccfldextdgrr  31644  cmpcref  31702  eulerpartgbij  32239  eulerpartlemr  32241  oddprm2  32535  dfdm5  33653  dfrn5  33654  imaindm  33659  dffix2  34134  fixcnv  34137  dfom5b  34141  fnimage  34158  brimg  34166  bj-csbsnlem  35015  bj-projun  35111  bj-pw0ALT  35149  bj-vjust  35153  finxp1o  35490  iundif1  35678  poimirlem26  35730  csbcom2fi  36213  prtlem16  36810  sn-iotalem  40117  aaitgo  40903  imaiun1  41148  grumnueq  41794  nzss  41824  dfodd2  44976  dfeven5  45006  dfodd7  45007