Theorem eleq2d 2104

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

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1242   ∈ wcel 1390

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033

This theorem is referenced by:  eleq12d  2105  eleqtrd  2113  neleqtrd  2132  neleqtrrd  2133  abeq2d  2147  nfceqdf  2174  drnfc1  2191  drnfc2  2192  sbcbid  2810  cbvcsb  2850  sbcel1g  2863  csbeq2d  2868  csbie2g  2890  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  opeq1  3540  opeq2  3541  cbviun  3685  cbviin  3686  iinxsng  3721  iinxprg  3722  iunxsng  3723  cbvdisj  3746  mpteq12f  3828  axpweq  3915  rabxfrd  4167  onsucelsucexmid  4215  ordsucunielexmid  4216  0nelelxp  4316  opeliunxp  4338  opeliunxp2  4419  iunxpf  4427  elreimasng  4634  elimasng  4636  xpimasn  4712  ressn  4801  funfni  4942  fnbr  4944  fun11iun  5090  fvelrnb  5164  fvun1  5182  fvco2  5185  elpreima  5229  dff3im  5255  fmptco  5273  funfvima3  5335  eluniimadm  5347  dff13  5350  f1eqcocnv  5374  isoini  5400  riotaeqdv  5412  mpt2eq123dva  5508  cbvmpt2x  5524  ovelrn  5591  elovmpt2  5643  fmpt2x  5768  mpt2xopn0yelv  5795  mpt2xopovel  5797  isprmpt2  5799  rntpos  5813  smoel  5856  smoiso  5858  smoel2  5859  tfrlem9  5876  tfrlemisucaccv  5880  tfrlemiubacc  5885  tfrlemi14d  5888  tfri2d  5891  freceq1  5919  freceq2  5920  frec0g  5922  frecsuclem3  5929  frecsuc  5930  nnsucelsuc  6009  nnmordi  6025  ereldm  6085  iinerm  6114  archnqq  6400  ltdfpr  6488  genpelxp  6493  genpelvl  6494  genpelvu  6495  addcanprleml  6587  addcanprlemu  6588  cauappcvgprlem1  6630  eluz1  8233  elixx1  8516  elioo2  8540  elfz1  8629  elfzp1  8684  fzpr  8689  fzsuc2  8691  fzrev3  8699  elfzp12  8711  fzm1  8712  fzoval  8755  elfzo  8756  elfzom1b  8835  fzosplitsni  8841  frecuzrdgfn  8859  bj-sels  9345