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  10060  fzoss2  10171  fzosubel3  10195  elfzomin  10205  elfzonlteqm1  10209  fzoend  10221  fzofzp1  10226  fzofzp1b  10227  peano2fzor  10231  zmodfzo  10346  frecuzrdg0  10412  frecuzrdgsuc  10413  frecuzrdgdomlem  10416  frecuzrdg0t  10421  frecuzrdgsuctlem  10422  seq3f1olemqsum  10499  bcn2  10743  summodclem2a  11388  fisumss  11399  fsumm1  11423  fisumcom2  11445  prodmodclem2a  11583  fprodm1  11605  fprodcom2fi  11633  ennnfonelemex  12414  ctinfomlemom  12427  mndpropd  12840  grpsubpropd2  12974  subg0  13038  issubg2m  13047  srgpcomp  13171  srgpcompp  13172  srgpcomppsc  13173  ringpropd  13215  mulgass3  13252  lringuplu  13335  aprcotr  13373  lmtopcnp  13720  txopn  13735  blpnfctr  13909  metcnpi  13985  metcnpi2  13986  cncfmpt2fcntop  14055  limcimolemlt  14103  cnplimclemr  14108  limccnp2lem  14115  limccnp2cntop  14116  dvidlemap  14130  dvcnp2cntop  14133  dvcn  14134  dvaddxxbr  14135  dvmulxxbr  14136  dvef  14158