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  4221  0nelop  4233  tfisi  4571  nnpredlt  4608  iotam  5190  ercl  6524  erth  6557  ecelqsdm  6583  phpm  6843  exmidpweq  6887  cc2lem  7228  cc3  7230  suplocexprlemmu  7680  suplocexprlemloc  7683  lincmb01cmp  9960  fzopth  10017  fzoaddel2  10149  fzosubel2  10151  fzocatel  10155  zpnn0elfzo1  10164  fzoend  10178  peano2fzor  10188  monoord2  10433  ser3mono  10434  bcpasc  10700  zfz1isolemiso  10774  fisum0diag2  11410  isumsplit  11454  prodmodclem3  11538  prodmodclem2a  11539  nnmindc  11989  nnminle  11990  basmexd  12475  mgm1  12624  grpidd  12637  ismndd  12673  mndpropd  12676  grpidd2  12744  iscnp4  13012  cnrest2r  13031  txbasval  13061  txlm  13073  xmetunirn  13152  xblss2ps  13198  blbas  13227  mopntopon  13237  isxms2  13246  metcnpi  13309  metcnpi2  13310  tgioo  13340  cncfmpt2fcntop  13379  limccl  13422  limcimolemlt  13427  limccnp2cntop  13440  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471