Theorem eleqtrrd 2276

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  3eltr4d  2280  rspc2vd  3153  exmidsssnc  4237  tfrexlem  6401  nnsucuniel  6562  erref  6621  en1uniel  6872  fin0  6955  fin0or  6956  prarloclemarch2  7503  fzopth  10153  fzoss2  10265  fzosubel3  10289  elfzomin  10299  elfzonlteqm1  10303  fzoend  10315  fzofzp1  10320  fzofzp1b  10321  peano2fzor  10325  zmodfzo  10456  frecuzrdg0  10522  frecuzrdgsuc  10523  frecuzrdgdomlem  10526  frecuzrdg0t  10531  frecuzrdgsuctlem  10532  seq3f1olemqsum  10622  seqf1oglem2  10629  bcn2  10873  summodclem2a  11563  fisumss  11574  fsumm1  11598  fisumcom2  11620  prodmodclem2a  11758  fprodm1  11780  fprodcom2fi  11808  ennnfonelemex  12656  ctinfomlemom  12669  strslfv3  12749  gsumpropd2  13095  sgrppropd  13115  mndpropd  13142  imasmnd  13155  grpsubpropd2  13307  imasgrp  13317  subg0  13386  issubg2m  13395  ghmrn  13463  0ghm  13464  resghm2  13467  ghmco  13470  rngpropd  13587  imasrng  13588  srgpcomp  13622  srgpcompp  13623  srgpcomppsc  13624  ringpropd  13670  imasring  13696  qusring2  13698  mulgass3  13717  rhmopp  13808  lringuplu  13828  aprcotr  13917  lmodprop2d  13980  islssmd  13991  2idl0  14144  2idl1  14145  qus2idrng  14157  qus1  14158  qusrhm  14160  znf1o  14283  psrbaglesuppg  14302  psr0cl  14309  psrnegcl  14311  psr1clfi  14316  lmtopcnp  14570  txopn  14585  blpnfctr  14759  metcnpi  14835  metcnpi2  14836  cncfmpt2fcntop  14919  limcimolemlt  14984  cnplimclemr  14989  limccnp2lem  14996  limccnp2cntop  14997  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvcn  15020  dvaddxxbr  15021  dvmulxxbr  15022  dvef  15047  lgseisenlem3  15397  lgseisenlem4  15398