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  6394  nnsucuniel  6555  erref  6614  en1uniel  6865  fin0  6948  fin0or  6949  prarloclemarch2  7489  fzopth  10139  fzoss2  10251  fzosubel3  10275  elfzomin  10285  elfzonlteqm1  10289  fzoend  10301  fzofzp1  10306  fzofzp1b  10307  peano2fzor  10311  zmodfzo  10442  frecuzrdg0  10508  frecuzrdgsuc  10509  frecuzrdgdomlem  10512  frecuzrdg0t  10517  frecuzrdgsuctlem  10518  seq3f1olemqsum  10608  seqf1oglem2  10615  bcn2  10859  summodclem2a  11549  fisumss  11560  fsumm1  11584  fisumcom2  11606  prodmodclem2a  11744  fprodm1  11766  fprodcom2fi  11794  ennnfonelemex  12642  ctinfomlemom  12655  strslfv3  12735  gsumpropd2  13062  sgrppropd  13082  mndpropd  13107  grpsubpropd2  13263  imasgrp  13267  subg0  13336  issubg2m  13345  ghmrn  13413  0ghm  13414  resghm2  13417  ghmco  13420  rngpropd  13537  imasrng  13538  srgpcomp  13572  srgpcompp  13573  srgpcomppsc  13574  ringpropd  13620  imasring  13646  qusring2  13648  mulgass3  13667  rhmopp  13758  lringuplu  13778  aprcotr  13867  lmodprop2d  13930  islssmd  13941  2idl0  14094  2idl1  14095  qus2idrng  14107  qus1  14108  qusrhm  14110  znf1o  14233  psrbaglesuppg  14252  lmtopcnp  14512  txopn  14527  blpnfctr  14701  metcnpi  14777  metcnpi2  14778  cncfmpt2fcntop  14861  limcimolemlt  14926  cnplimclemr  14931  limccnp2lem  14938  limccnp2cntop  14939  dvidlemap  14953  dvidrelem  14954  dvidsslem  14955  dvcnp2cntop  14961  dvcn  14962  dvaddxxbr  14963  dvmulxxbr  14964  dvef  14989  lgseisenlem3  15339  lgseisenlem4  15340