Theorem eleqtrrd 2219

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 2145	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2218	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  3eltr4d  2223  exmidsssnc  4126  tfrexlem  6231  nnsucuniel  6391  erref  6449  en1uniel  6698  fin0  6779  fin0or  6780  prarloclemarch2  7227  fzopth  9841  fzoss2  9949  fzosubel3  9973  elfzomin  9983  elfzonlteqm1  9987  fzoend  9999  fzofzp1  10004  fzofzp1b  10005  peano2fzor  10009  zmodfzo  10120  frecuzrdg0  10186  frecuzrdgsuc  10187  frecuzrdgdomlem  10190  frecuzrdg0t  10195  frecuzrdgsuctlem  10196  seq3f1olemqsum  10273  bcn2  10510  summodclem2a  11150  fisumss  11161  fsumm1  11185  fisumcom2  11207  prodmodclem2a  11345  ennnfonelemex  11927  ctinfomlemom  11940  lmtopcnp  12419  txopn  12434  blpnfctr  12608  metcnpi  12684  metcnpi2  12685  cncfmpt2fcntop  12754  limcimolemlt  12802  cnplimclemr  12807  limccnp2lem  12814  limccnp2cntop  12815  dvidlemap  12829  dvcnp2cntop  12832  dvcn  12833  dvaddxxbr  12834  dvmulxxbr  12835  dvef  12856