Theorem eleqtrd 2244

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

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleqtrrd  2245  3eltr3d  2248  eleqtrid  2254  eleqtrdi  2258  opth1  4213  0nelop  4225  tfisi  4563  nnpredlt  4600  ercl  6508  erth  6541  ecelqsdm  6567  phpm  6827  exmidpweq  6871  cc2lem  7203  cc3  7205  suplocexprlemmu  7655  suplocexprlemloc  7658  lincmb01cmp  9935  fzopth  9992  fzoaddel2  10124  fzosubel2  10126  fzocatel  10130  zpnn0elfzo1  10139  fzoend  10153  peano2fzor  10163  monoord2  10408  ser3mono  10409  bcpasc  10675  zfz1isolemiso  10748  fisum0diag2  11384  isumsplit  11428  prodmodclem3  11512  prodmodclem2a  11513  nnmindc  11963  nnminle  11964  iscnp4  12818  cnrest2r  12837  txbasval  12867  txlm  12879  xmetunirn  12958  xblss2ps  13004  blbas  13033  mopntopon  13043  isxms2  13052  metcnpi  13115  metcnpi2  13116  tgioo  13146  cncfmpt2fcntop  13185  limccl  13228  limcimolemlt  13233  limccnp2cntop  13246  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277