Theorem eleqtrrd 2257

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  3eltr4d  2261  rspc2vd  3125  exmidsssnc  4203  tfrexlem  6334  nnsucuniel  6495  erref  6554  en1uniel  6803  fin0  6884  fin0or  6885  prarloclemarch2  7417  fzopth  10058  fzoss2  10169  fzosubel3  10193  elfzomin  10203  elfzonlteqm1  10207  fzoend  10219  fzofzp1  10224  fzofzp1b  10225  peano2fzor  10229  zmodfzo  10344  frecuzrdg0  10410  frecuzrdgsuc  10411  frecuzrdgdomlem  10414  frecuzrdg0t  10419  frecuzrdgsuctlem  10420  seq3f1olemqsum  10497  bcn2  10739  summodclem2a  11384  fisumss  11395  fsumm1  11419  fisumcom2  11441  prodmodclem2a  11579  fprodm1  11601  fprodcom2fi  11629  ennnfonelemex  12409  ctinfomlemom  12422  mndpropd  12795  grpsubpropd2  12929  subg0  12993  issubg2m  13002  srgpcomp  13126  srgpcompp  13127  srgpcomppsc  13128  ringpropd  13170  mulgass3  13207  lringuplu  13290  aprcotr  13296  lmtopcnp  13643  txopn  13658  blpnfctr  13832  metcnpi  13908  metcnpi2  13909  cncfmpt2fcntop  13978  limcimolemlt  14026  cnplimclemr  14031  limccnp2lem  14038  limccnp2cntop  14039  dvidlemap  14053  dvcnp2cntop  14056  dvcn  14057  dvaddxxbr  14058  dvmulxxbr  14059  dvef  14081