Theorem eqriv 2757

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  eqid  2760  cbvabv  2830  cbvabw  2831  cbvab  2832  vjust  3451  rabtru  3642  nfccdeq  3735  csbgfi  3866  difeqri  4065  ineqri  4109  uneqri  4155  symdifass  4207  indifdi  4239  undif3  4245  csbcom  4377  csbab  4397  pwv  4574  pwpr  4827  pwtp  4828  uniun  4889  int0  4921  intun  4939  iuncom  4958  iuncom4  4959  iunin2  5028  iinun2  5030  iundif2  5031  iunun  5052  iunxun  5053  iunxiun  5056  iinpw  5065  inuni  5310  unipw  5417  xpiundi  5721  xpiundir  5722  iunxpf  5825  cnvuni  5867  dmiun  5894  dmuni  5895  idinxpres  6038  rniun  6138  xpdifid  6158  xpdifcnvepel  6159  cnvresima  6231  imaco  6252  rnco  6253  rncoOLD  6254  imaindm  6302  dfmpt3  6673  imaiun  7249  unon  7842  opabex3d  7977  opabex3rd  7978  opabex3  7979  fparlem1  8125  fparlem2  8126  oarec  8573  ecid  8804  qsid  8805  mapval2  8903  ixpin  8954  onfin2  9235  unfilem1  9300  unifpw  9347  dfom5  9654  alephsuc2  10162  ackbij2  10323  isf33lem  10447  dffin7-2  10479  fin1a2lem6  10486  acncc  10521  fin41  10525  iunfo  10626  grutsk  10910  grothac  10918  grothtsk  10923  dfz2  12715  qexALT  13094  dfrp2  13528  om2uzrani  14098  hashkf  14479  divalglem4  16571  1nprm  16859  nsgacs  19377  oppgsubm  19581  oppgsubg  19582  oppgcntz  19583  pmtrprfvalrn  19707  opprsubg  20587  opprunit  20612  opprirred  20657  rimval  20735  dfric2  20762  opprsubrng  20816  opprsubrg  20850  00lss  21221  dfprm2  21784  unocv  21991  iunocv  21992  00ply1bas  22562  toprntopon  23248  unisngl  23851  zcld  25138  iundisj  25874  plyun0  26520  aannenlem2  26661  dfz12s2  28879  eqid1  31073  choc0  31933  chocnul  31935  spanunsni  32186  lncnbd  32645  adjbd1o  32692  rnbra  32714  pjimai  32783  iunin1f  33199  iundisjf  33230  xrdifh  33418  iundisjfi  33434  opprnsg  34054  0mplrim  34192  ccfldextdgrr  34350  cmpcref  34528  eulerpartgbij  35050  eulerpartlemr  35052  oddprm2  35330  dfdm5  36629  dfrn5  36630  dffix2  36759  fixcnv  36762  dfom5b  36766  fnimage  36783  brimg  36791  bj-csbsnlem  37907  bj-projun  37999  coi1in  38053  bj-pw0ALT  38056  bj-vjust  38062  finxp1o  38408  iundif1  38615  poimirlem26  38657  csbcom2fi  39153  dfsucmap3  39488  prtlem16  40019  sn-iotalem  43368  redvmptabs  43504  aaitgo  44257  imaiun1  44744  grumnueq  45364  nzss  45394  wrddin2  47991  chndin2  47996  chnrin2  48001  dfodd2  48827  dfeven5  48857  dfodd7  48858  dfidom2  49533  ixpv  50096  isoval2  50242  oppcciceq  50259  oppczeroo  50452  dfinito4  50729  lmdfval2  50931  cmdfval2  50932  initocmd  50945  termolmd  50946