Theorem eleqtrrd 2311

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  3eltr4d  2315  rspc2vd  3196  exmidsssnc  4293  funopsn  5829  tfrexlem  6499  nnsucuniel  6662  erref  6721  en1uniel  6977  fin0  7073  fin0or  7074  pw1if  7442  prarloclemarch2  7638  fzopth  10295  fzoss2  10408  fz1fzo0m1  10427  fzo0addel  10432  fzo0addelr  10433  elfzoext  10436  fzosubel3  10440  elfzomin  10450  elfzonlteqm1  10454  fzoend  10466  fzofzp1  10471  fzofzp1b  10472  peano2fzor  10476  zmodfzo  10608  frecuzrdg0  10674  frecuzrdgsuc  10675  frecuzrdgdomlem  10678  frecuzrdg0t  10683  frecuzrdgsuctlem  10684  seq3f1olemqsum  10774  seqf1oglem2  10781  bcn2  11025  ccats1val2  11216  swrdccat2  11251  pfxccat1  11282  swrdswrd  11285  pfxccatin12  11313  summodclem2a  11941  fisumss  11952  fsumm1  11976  fisumcom2  11998  prodmodclem2a  12136  fprodm1  12158  fprodcom2fi  12186  ennnfonelemex  13034  ctinfomlemom  13047  strslfv3  13127  bassetsnn  13138  gsumpropd2  13475  sgrppropd  13495  mndpropd  13522  imasmnd  13535  grpsubpropd2  13687  imasgrp  13697  subg0  13766  issubg2m  13775  ghmrn  13843  0ghm  13844  resghm2  13847  ghmco  13850  rngpropd  13967  imasrng  13968  srgpcomp  14002  srgpcompp  14003  srgpcomppsc  14004  ringpropd  14050  imasring  14076  qusring2  14078  mulgass3  14097  rhmopp  14189  lringuplu  14209  aprcotr  14298  lmodprop2d  14361  islssmd  14372  2idl0  14525  2idl1  14526  qus2idrng  14538  qus1  14539  qusrhm  14541  znf1o  14664  psrbaglesuppg  14685  psr0cl  14694  psrnegcl  14696  psr1clfi  14701  mplsubgfilemm  14711  lmtopcnp  14973  txopn  14988  blpnfctr  15162  metcnpi  15238  metcnpi2  15239  cncfmpt2fcntop  15322  limcimolemlt  15387  cnplimclemr  15392  limccnp2lem  15399  limccnp2cntop  15400  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvcn  15423  dvaddxxbr  15424  dvmulxxbr  15425  dvef  15450  lgseisenlem3  15800  lgseisenlem4  15801  iedgedgg  15911  upgrex  15953  upgr1eopdc  15973  upgr1een  15974  umgr1een  15975  usgredg3  16064  uspgr1eopdc  16093  usgr1eop  16095  vtxdfifiun  16147  1loopgruspgr  16153  1loopgrvd2fi  16155  1loopgrvd0fi  16156  1hevtxdg0fi  16157  1hevtxdg1en  16158  1hegrvtxdg1fi  16159  edginwlkd  16205  wlkres  16229