Theorem eqriv 2758

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  eqid  2761  cbvabv  2831  cbvabw  2832  cbvab  2833  vjust  3452  rabtru  3643  nfccdeq  3736  csbgfi  3867  difeqri  4076  uneqri  4103  ineqri  4158  symdifass  4208  indifdi  4240  undif3  4246  csbcom  4378  csbab  4398  pwpr  4861  pwtp  4862  pwv  4864  uniun  4890  int0  4922  intun  4940  iuncom  4959  iuncom4  4960  iunin2  5029  iinun2  5031  iundif2  5032  iunun  5053  iunxun  5054  iunxiun  5057  iinpw  5066  inuni  5311  unipw  5418  xpiundi  5722  xpiundir  5723  iunxpf  5826  cnvuni  5868  dmiun  5895  dmuni  5896  idinxpres  6039  rniun  6139  xpdifid  6159  xpdifcnvepel  6160  cnvresima  6231  imaco  6252  rnco  6253  rncoOLD  6254  imaindm  6302  dfmpt3  6673  imaiun  7249  unon  7842  opabex3d  7977  opabex3rd  7978  opabex3  7979  fparlem1  8123  fparlem2  8124  oarec  8570  ecid  8801  qsid  8802  mapval2  8900  ixpin  8951  onfin2  9232  unfilem1  9297  unifpw  9344  dfom5  9651  alephsuc2  10159  ackbij2  10320  isf33lem  10444  dffin7-2  10476  fin1a2lem6  10483  acncc  10518  fin41  10522  iunfo  10623  grutsk  10907  grothac  10915  grothtsk  10920  dfz2  12712  qexALT  13091  dfrp2  13525  om2uzrani  14095  hashkf  14476  divalglem4  16566  1nprm  16854  nsgacs  19372  oppgsubm  19576  oppgsubg  19577  oppgcntz  19578  pmtrprfvalrn  19702  opprsubg  20582  opprunit  20607  opprirred  20652  rimval  20730  dfric2  20757  opprsubrng  20811  opprsubrg  20845  00lss  21216  dfprm2  21779  unocv  21986  iunocv  21987  00ply1bas  22557  toprntopon  23243  unisngl  23846  zcld  25133  iundisj  25869  plyun0  26515  aannenlem2  26656  dfz12s2  28874  eqid1  31068  choc0  31928  chocnul  31930  spanunsni  32181  lncnbd  32640  adjbd1o  32687  rnbra  32709  pjimai  32778  iunin1f  33152  iundisjf  33183  xrdifh  33372  iundisjfi  33388  opprnsg  34008  0mplrim  34146  ccfldextdgrr  34304  cmpcref  34482  eulerpartgbij  35004  eulerpartlemr  35006  oddprm2  35284  dfdm5  36537  dfrn5  36538  dffix2  36667  fixcnv  36670  dfom5b  36674  fnimage  36691  brimg  36699  bj-csbsnlem  37815  bj-projun  37907  coi1in  37961  bj-pw0ALT  37964  bj-vjust  37970  finxp1o  38315  iundif1  38522  poimirlem26  38564  csbcom2fi  39060  dfsucmap3  39395  prtlem16  39926  sn-iotalem  43275  redvmptabs  43411  aaitgo  44163  imaiun1  44650  grumnueq  45270  nzss  45300  wrddin2  47897  chndin2  47902  chnrin2  47907  dfodd2  48733  dfeven5  48763  dfodd7  48764  dfidom2  49439  ixpv  49997  isoval2  50142  oppcciceq  50159  oppczeroo  50344  dfinito4  50608  lmdfval2  50762  cmdfval2  50763  initocmd  50776  termolmd  50777