Theorem eleqtrd 2216

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eleqtrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2207	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 146	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  eleqtrrd  2217  3eltr3d  2220  eleqtrid  2226  eleqtrdi  2230  opth1  4153  0nelop  4165  tfisi  4496  ercl  6433  erth  6466  ecelqsdm  6492  phpm  6752  suplocexprlemmu  7519  suplocexprlemloc  7522  lincmb01cmp  9779  fzopth  9834  fzoaddel2  9963  fzosubel2  9965  fzocatel  9969  zpnn0elfzo1  9978  fzoend  9992  peano2fzor  10002  monoord2  10243  ser3mono  10244  bcpasc  10505  zfz1isolemiso  10575  fisum0diag2  11209  isumsplit  11253  iscnp4  12376  cnrest2r  12395  txbasval  12425  txlm  12437  xmetunirn  12516  xblss2ps  12562  blbas  12591  mopntopon  12601  isxms2  12610  metcnpi  12673  metcnpi2  12674  tgioo  12704  cncfmpt2fcntop  12743  limccl  12786  limcimolemlt  12791  limccnp2cntop  12804  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvrecap  12835