Theorem eleq2d 2085

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eleq2d	⊢ (φ → (𝐶 ∈ A ↔ 𝐶 ∈ B))

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (φ → A = B)
2		eleq2 2079	. 2 ⊢ (A = B → (𝐶 ∈ A ↔ 𝐶 ∈ B))
3	1, 2	syl 14	1 ⊢ (φ → (𝐶 ∈ A ↔ 𝐶 ∈ B))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1226   ∈ wcel 1370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-cleq 2011  df-clel 2014

This theorem is referenced by:  eleq12d  2086  eleqtrd  2094  neleqtrd  2113  neleqtrrd  2114  abeq2d  2128  nfceqdf  2155  drnfc1  2172  drnfc2  2173  sbcbid  2789  cbvcsb  2829  sbcel1g  2842  csbeq2d  2847  csbie2g  2869  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  opeq1  3519  opeq2  3520  cbviun  3664  cbviin  3665  iinxsng  3700  iinxprg  3701  iunxsng  3702  cbvdisj  3725  mpteq12f  3807  axpweq  3894  rabxfrd  4147  onsucelsucexmid  4195  ordsucunielexmid  4196  0nelelxp  4296  opeliunxp  4318  opeliunxp2  4399  iunxpf  4407  elreimasng  4614  elimasng  4616  xpimasn  4692  ressn  4781  funfni  4921  fnbr  4923  fun11iun  5068  fvelrnb  5142  fvun1  5160  fvco2  5163  elpreima  5207  dff3im  5233  fmptco  5251  funfvima3  5313  eluniimadm  5325  dff13  5328  f1eqcocnv  5352  isoini  5378  riotaeqdv  5390  mpt2eq123dva  5485  cbvmpt2x  5501  ovelrn  5568  elovmpt2  5620  fmpt2x  5745  mpt2xopn0yelv  5772  mpt2xopovel  5774  isprmpt2  5776  rntpos  5790  smoel  5833  smoiso  5835  smoel2  5836  tfrlem9  5853  tfrlemisucaccv  5856  tfrlemiubacc  5861  tfrlemi14d  5864  tfrlemi14  5865  tfri2d  5868  frec0g  5898  frecsuclem3  5902  frecsuc  5903  nnsucelsuc  5981  nnmordi  5996  ereldm  6056  iinerm  6085  archnqq  6268  ltdfpr  6354  genpelxp  6359  genpelvl  6360  genpelvu  6361  genpelpw  6365  addcanprleml  6445  addcanprlemu  6446  bj-sels  7276