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  4236  tfrexlem  6392  nnsucuniel  6553  erref  6612  en1uniel  6863  fin0  6946  fin0or  6947  prarloclemarch2  7486  fzopth  10136  fzoss2  10248  fzosubel3  10272  elfzomin  10282  elfzonlteqm1  10286  fzoend  10298  fzofzp1  10303  fzofzp1b  10304  peano2fzor  10308  zmodfzo  10439  frecuzrdg0  10505  frecuzrdgsuc  10506  frecuzrdgdomlem  10509  frecuzrdg0t  10514  frecuzrdgsuctlem  10515  seq3f1olemqsum  10605  seqf1oglem2  10612  bcn2  10856  summodclem2a  11546  fisumss  11557  fsumm1  11581  fisumcom2  11603  prodmodclem2a  11741  fprodm1  11763  fprodcom2fi  11791  ennnfonelemex  12631  ctinfomlemom  12644  gsumpropd2  13036  sgrppropd  13056  mndpropd  13081  grpsubpropd2  13237  imasgrp  13241  subg0  13310  issubg2m  13319  ghmrn  13387  0ghm  13388  resghm2  13391  ghmco  13394  rngpropd  13511  imasrng  13512  srgpcomp  13546  srgpcompp  13547  srgpcomppsc  13548  ringpropd  13594  imasring  13620  qusring2  13622  mulgass3  13641  rhmopp  13732  lringuplu  13752  aprcotr  13841  lmodprop2d  13904  islssmd  13915  2idl0  14068  2idl1  14069  qus2idrng  14081  qus1  14082  qusrhm  14084  znf1o  14207  psrbaglesuppg  14226  lmtopcnp  14486  txopn  14501  blpnfctr  14675  metcnpi  14751  metcnpi2  14752  cncfmpt2fcntop  14835  limcimolemlt  14900  cnplimclemr  14905  limccnp2lem  14912  limccnp2cntop  14913  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvcn  14936  dvaddxxbr  14937  dvmulxxbr  14938  dvef  14963  lgseisenlem3  15313  lgseisenlem4  15314