Theorem eleqtrd 2249

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleqtrrd  2250  3eltr3d  2253  eleqtrid  2259  eleqtrdi  2263  opth1  4219  0nelop  4231  tfisi  4569  nnpredlt  4606  iotam  5188  ercl  6522  erth  6555  ecelqsdm  6581  phpm  6841  exmidpweq  6885  cc2lem  7221  cc3  7223  suplocexprlemmu  7673  suplocexprlemloc  7676  lincmb01cmp  9953  fzopth  10010  fzoaddel2  10142  fzosubel2  10144  fzocatel  10148  zpnn0elfzo1  10157  fzoend  10171  peano2fzor  10181  monoord2  10426  ser3mono  10427  bcpasc  10693  zfz1isolemiso  10767  fisum0diag2  11403  isumsplit  11447  prodmodclem3  11531  prodmodclem2a  11532  nnmindc  11982  nnminle  11983  basmexd  12468  mgm1  12617  grpidd  12630  ismndd  12666  mndpropd  12669  grpidd2  12737  iscnp4  12977  cnrest2r  12996  txbasval  13026  txlm  13038  xmetunirn  13117  xblss2ps  13163  blbas  13192  mopntopon  13202  isxms2  13211  metcnpi  13274  metcnpi2  13275  tgioo  13305  cncfmpt2fcntop  13344  limccl  13387  limcimolemlt  13392  limccnp2cntop  13405  dvmulxxbr  13425  dvcoapbr  13430  dvcjbr  13431  dvrecap  13436