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  7505  fzopth  10155  fzoss2  10267  fzosubel3  10291  elfzomin  10301  elfzonlteqm1  10305  fzoend  10317  fzofzp1  10322  fzofzp1b  10323  peano2fzor  10327  zmodfzo  10458  frecuzrdg0  10524  frecuzrdgsuc  10525  frecuzrdgdomlem  10528  frecuzrdg0t  10533  frecuzrdgsuctlem  10534  seq3f1olemqsum  10624  seqf1oglem2  10631  bcn2  10875  summodclem2a  11565  fisumss  11576  fsumm1  11600  fisumcom2  11622  prodmodclem2a  11760  fprodm1  11782  fprodcom2fi  11810  ennnfonelemex  12658  ctinfomlemom  12671  strslfv3  12751  gsumpropd2  13097  sgrppropd  13117  mndpropd  13144  imasmnd  13157  grpsubpropd2  13309  imasgrp  13319  subg0  13388  issubg2m  13397  ghmrn  13465  0ghm  13466  resghm2  13469  ghmco  13472  rngpropd  13589  imasrng  13590  srgpcomp  13624  srgpcompp  13625  srgpcomppsc  13626  ringpropd  13672  imasring  13698  qusring2  13700  mulgass3  13719  rhmopp  13810  lringuplu  13830  aprcotr  13919  lmodprop2d  13982  islssmd  13993  2idl0  14146  2idl1  14147  qus2idrng  14159  qus1  14160  qusrhm  14162  znf1o  14285  psrbaglesuppg  14306  psr0cl  14315  psrnegcl  14317  psr1clfi  14322  mplsubgfilemm  14332  lmtopcnp  14594  txopn  14609  blpnfctr  14783  metcnpi  14859  metcnpi2  14860  cncfmpt2fcntop  14943  limcimolemlt  15008  cnplimclemr  15013  limccnp2lem  15020  limccnp2cntop  15021  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvcn  15044  dvaddxxbr  15045  dvmulxxbr  15046  dvef  15071  lgseisenlem3  15421  lgseisenlem4  15422