Theorem eleqtrrd 2273

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  3eltr4d  2277  rspc2vd  3149  exmidsssnc  4232  tfrexlem  6387  nnsucuniel  6548  erref  6607  en1uniel  6858  fin0  6941  fin0or  6942  prarloclemarch2  7479  fzopth  10127  fzoss2  10239  fzosubel3  10263  elfzomin  10273  elfzonlteqm1  10277  fzoend  10289  fzofzp1  10294  fzofzp1b  10295  peano2fzor  10299  zmodfzo  10418  frecuzrdg0  10484  frecuzrdgsuc  10485  frecuzrdgdomlem  10488  frecuzrdg0t  10493  frecuzrdgsuctlem  10494  seq3f1olemqsum  10584  seqf1oglem2  10591  bcn2  10835  summodclem2a  11524  fisumss  11535  fsumm1  11559  fisumcom2  11581  prodmodclem2a  11719  fprodm1  11741  fprodcom2fi  11769  ennnfonelemex  12571  ctinfomlemom  12584  gsumpropd2  12976  sgrppropd  12996  mndpropd  13021  grpsubpropd2  13177  imasgrp  13181  subg0  13250  issubg2m  13259  ghmrn  13327  0ghm  13328  resghm2  13331  ghmco  13334  rngpropd  13451  imasrng  13452  srgpcomp  13486  srgpcompp  13487  srgpcomppsc  13488  ringpropd  13534  imasring  13560  qusring2  13562  mulgass3  13581  rhmopp  13672  lringuplu  13692  aprcotr  13781  lmodprop2d  13844  islssmd  13855  2idl0  14008  2idl1  14009  qus2idrng  14021  qus1  14022  qusrhm  14024  znf1o  14139  psrbaglesuppg  14158  lmtopcnp  14418  txopn  14433  blpnfctr  14607  metcnpi  14683  metcnpi2  14684  cncfmpt2fcntop  14753  limcimolemlt  14818  cnplimclemr  14823  limccnp2lem  14830  limccnp2cntop  14831  dvidlemap  14845  dvcnp2cntop  14848  dvcn  14849  dvaddxxbr  14850  dvmulxxbr  14851  dvef  14873  lgseisenlem3  15188  lgseisenlem4  15189