Theorem eleqtrrd 2246

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eleqtrrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrd

Step	Hyp	Ref	Expression
1		eleqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2171	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2245	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:  3eltr4d  2250  exmidsssnc  4182  tfrexlem  6302  nnsucuniel  6463  erref  6521  en1uniel  6770  fin0  6851  fin0or  6852  prarloclemarch2  7360  fzopth  9996  fzoss2  10107  fzosubel3  10131  elfzomin  10141  elfzonlteqm1  10145  fzoend  10157  fzofzp1  10162  fzofzp1b  10163  peano2fzor  10167  zmodfzo  10282  frecuzrdg0  10348  frecuzrdgsuc  10349  frecuzrdgdomlem  10352  frecuzrdg0t  10357  frecuzrdgsuctlem  10358  seq3f1olemqsum  10435  bcn2  10677  summodclem2a  11322  fisumss  11333  fsumm1  11357  fisumcom2  11379  prodmodclem2a  11517  fprodm1  11539  fprodcom2fi  11567  ennnfonelemex  12347  ctinfomlemom  12360  lmtopcnp  12890  txopn  12905  blpnfctr  13079  metcnpi  13155  metcnpi2  13156  cncfmpt2fcntop  13225  limcimolemlt  13273  cnplimclemr  13278  limccnp2lem  13285  limccnp2cntop  13286  dvidlemap  13300  dvcnp2cntop  13303  dvcn  13304  dvaddxxbr  13305  dvmulxxbr  13306  dvef  13328