Theorem eleqtrrd 2250

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 2176	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2249	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:  3eltr4d  2254  rspc2vd  3117  exmidsssnc  4189  tfrexlem  6313  nnsucuniel  6474  erref  6533  en1uniel  6782  fin0  6863  fin0or  6864  prarloclemarch2  7381  fzopth  10017  fzoss2  10128  fzosubel3  10152  elfzomin  10162  elfzonlteqm1  10166  fzoend  10178  fzofzp1  10183  fzofzp1b  10184  peano2fzor  10188  zmodfzo  10303  frecuzrdg0  10369  frecuzrdgsuc  10370  frecuzrdgdomlem  10373  frecuzrdg0t  10378  frecuzrdgsuctlem  10379  seq3f1olemqsum  10456  bcn2  10698  summodclem2a  11344  fisumss  11355  fsumm1  11379  fisumcom2  11401  prodmodclem2a  11539  fprodm1  11561  fprodcom2fi  11589  ennnfonelemex  12369  ctinfomlemom  12382  mndpropd  12676  lmtopcnp  13044  txopn  13059  blpnfctr  13233  metcnpi  13309  metcnpi2  13310  cncfmpt2fcntop  13379  limcimolemlt  13427  cnplimclemr  13432  limccnp2lem  13439  limccnp2cntop  13440  dvidlemap  13454  dvcnp2cntop  13457  dvcn  13458  dvaddxxbr  13459  dvmulxxbr  13460  dvef  13482