Theorem eleq2d 2107

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

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq2d	⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eleq2 2101	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243   ∈ wcel 1393

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

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

This theorem is referenced by:  eleq12d  2108  eleqtrd  2116  neleqtrd  2135  neleqtrrd  2136  abeq2d  2150  nfceqdf  2177  drnfc1  2194  drnfc2  2195  sbcbid  2816  cbvcsb  2856  sbcel1g  2869  csbeq2d  2874  csbie2g  2896  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  opeq1  3549  opeq2  3550  cbviun  3694  cbviin  3695  iinxsng  3730  iinxprg  3731  iunxsng  3732  cbvdisj  3755  mpteq12f  3837  axpweq  3924  rabxfrd  4201  onsucelsucexmid  4255  ordsucunielexmid  4256  0elsucexmid  4289  0nelelxp  4373  opeliunxp  4395  opeliunxp2  4476  iunxpf  4484  elreimasng  4691  elimasng  4693  xpimasn  4769  ressn  4858  funfni  4999  fnbr  5001  fun11iun  5147  fvelrnb  5221  fvun1  5239  fvco2  5242  elpreima  5286  dff3im  5312  fmptco  5330  funfvima3  5392  eluniimadm  5404  dff13  5407  f1eqcocnv  5431  isoini  5457  riotaeqdv  5469  mpt2eq123dva  5566  cbvmpt2x  5582  ovelrn  5649  elovmpt2  5701  fmpt2x  5826  mpt2xopn0yelv  5854  mpt2xopovel  5856  isprmpt2  5858  rntpos  5872  smoel  5915  smoiso  5917  smoel2  5918  tfrlem9  5935  tfrlemisucaccv  5939  tfrlemiubacc  5944  tfrlemi14d  5947  tfri2d  5950  freceq1  5979  freceq2  5980  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnsucelsuc  6070  nnmordi  6089  ereldm  6149  iinerm  6178  phplem4  6318  phplem3g  6319  phplem4on  6329  ordiso2  6355  archnqq  6513  ltdfpr  6602  genpelxp  6607  genpelvl  6608  genpelvu  6609  addcanprleml  6710  addcanprlemu  6711  cauappcvgprlem1  6755  eluz1  8475  elixx1  8764  elioo2  8788  elfz1  8877  elfzp1  8932  fzpr  8937  fzsuc2  8939  fzrev3  8947  elfzp12  8959  fzm1  8960  fzoval  9003  elfzo  9004  elfzom1b  9083  fzosplitsni  9089  frecuzrdgfn  9172  shftfn  9399  shftval  9400  sumeq1  9848  ialgfx  9865  bj-sels  10008