Theorem eleqtrd 2218

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 2209	. 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 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eleqtrrd  2219  3eltr3d  2222  eleqtrid  2228  eleqtrdi  2232  opth1  4158  0nelop  4170  tfisi  4501  ercl  6440  erth  6473  ecelqsdm  6499  phpm  6759  suplocexprlemmu  7526  suplocexprlemloc  7529  lincmb01cmp  9786  fzopth  9841  fzoaddel2  9970  fzosubel2  9972  fzocatel  9976  zpnn0elfzo1  9985  fzoend  9999  peano2fzor  10009  monoord2  10250  ser3mono  10251  bcpasc  10512  zfz1isolemiso  10582  fisum0diag2  11216  isumsplit  11260  prodmodclem3  11344  prodmodclem2a  11345  iscnp4  12387  cnrest2r  12406  txbasval  12436  txlm  12448  xmetunirn  12527  xblss2ps  12573  blbas  12602  mopntopon  12612  isxms2  12621  metcnpi  12684  metcnpi2  12685  tgioo  12715  cncfmpt2fcntop  12754  limccl  12797  limcimolemlt  12802  limccnp2cntop  12815  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvrecap  12846