Theorem eleqtrd 2219

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 2210	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 146	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

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

This theorem is referenced by:  eleqtrrd  2220  3eltr3d  2223  eleqtrid  2229  eleqtrdi  2233  opth1  4166  0nelop  4178  tfisi  4509  ercl  6448  erth  6481  ecelqsdm  6507  phpm  6767  cc2lem  7098  cc3  7100  suplocexprlemmu  7550  suplocexprlemloc  7553  lincmb01cmp  9816  fzopth  9872  fzoaddel2  10001  fzosubel2  10003  fzocatel  10007  zpnn0elfzo1  10016  fzoend  10030  peano2fzor  10040  monoord2  10281  ser3mono  10282  bcpasc  10544  zfz1isolemiso  10614  fisum0diag2  11248  isumsplit  11292  prodmodclem3  11376  prodmodclem2a  11377  iscnp4  12426  cnrest2r  12445  txbasval  12475  txlm  12487  xmetunirn  12566  xblss2ps  12612  blbas  12641  mopntopon  12651  isxms2  12660  metcnpi  12723  metcnpi2  12724  tgioo  12754  cncfmpt2fcntop  12793  limccl  12836  limcimolemlt  12841  limccnp2cntop  12854  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvrecap  12885