Theorem eleq2d 2083

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 2077	. 2 ⊢ (A = B → (𝐶 ∈ A ↔ 𝐶 ∈ B))
3	1, 2	syl 14	1 ⊢ (φ → (𝐶 ∈ A ↔ 𝐶 ∈ B))

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

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 1358  ax-ie2 1359  ax-4 1376  ax-17 1395  ax-ial 1403  ax-ext 1998

This theorem depends on definitions:  df-bi 110  df-cleq 2009  df-clel 2012

This theorem is referenced by:  eleq12d  2084  eleqtrd  2092  neleqtrd  2111  neleqtrrd  2112  abeq2d  2126  nfceqdf  2153  drnfc1  2170  drnfc2  2171  sbcbid  2787  cbvcsb  2827  sbcel1g  2840  csbeq2d  2845  csbie2g  2867  cbvralcsf  2879  cbvrexcsf  2880  cbvreucsf  2881  cbvrabcsf  2882  opeq1  3515  opeq2  3516  cbviun  3660  cbviin  3661  iinxsng  3696  iinxprg  3697  iunxsng  3698  cbvdisj  3721  mpteq12f  3803  axpweq  3890  rabxfrd  4142  onsucelsucexmid  4190  ordsucunielexmid  4191  0nelelxp  4291  opeliunxp  4313  opeliunxp2  4394  iunxpf  4402  elreimasng  4609  elimasng  4611  xpimasn  4687  ressn  4776  funfni  4916  fnbr  4918  fun11iun  5063  fvelrnb  5137  fvun1  5155  fvco2  5158  elpreima  5202  dff3im  5228  fmptco  5246  funfvima3  5308  eluniimadm  5320  dff13  5323  f1eqcocnv  5347  isoini  5373  riotaeqdv  5385  mpt2eq123dva  5480  cbvmpt2x  5496  ovelrn  5563  elovmpt2  5615  fmpt2x  5740  mpt2xopn0yelv  5767  mpt2xopovel  5769  isprmpt2  5771  rntpos  5785  smoel  5828  smoiso  5830  smoel2  5831  tfrlem9  5848  tfrlemisucaccv  5851  tfrlemiubacc  5856  tfrlemi14d  5859  tfrlemi14  5860  tfri2d  5863  frec0g  5893  frecsuclem3  5897  frecsuc  5898  nnsucelsuc  5976  nnmordi  5991  ereldm  6051  iinerm  6080  archnqq  6263  ltdfpr  6349  genpelxp  6354  genpelvl  6355  genpelvu  6356  genpelpw  6360  addcanprleml  6440  addcanprlemu  6441  elixx1  8245  elioo2  8269  bj-sels  8487