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 1398   ∈ 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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  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  3197  exmidsssnc  4299  funopsn  5838  tfrexlem  6543  nnsucuniel  6706  erref  6765  en1uniel  7021  fin0  7117  fin0or  7118  pw1if  7503  prarloclemarch2  7699  fzopth  10358  fzoss2  10471  fz1fzo0m1  10491  fzo0addel  10496  fzo0addelr  10497  elfzoext  10500  fzosubel3  10504  elfzomin  10514  elfzonlteqm1  10518  fzoend  10530  fzofzp1  10535  fzofzp1b  10536  peano2fzor  10540  zmodfzo  10672  frecuzrdg0  10738  frecuzrdgsuc  10739  frecuzrdgdomlem  10742  frecuzrdg0t  10747  frecuzrdgsuctlem  10748  seq3f1olemqsum  10838  seqf1oglem2  10845  bcn2  11089  ccats1val2  11283  swrdccat2  11318  pfxccat1  11349  swrdswrd  11352  pfxccatin12  11380  summodclem2a  12022  fisumss  12033  fsumm1  12057  fisumcom2  12079  prodmodclem2a  12217  fprodm1  12239  fprodcom2fi  12267  ennnfonelemex  13115  ctinfomlemom  13128  strslfv3  13208  bassetsnn  13219  gsumpropd2  13556  sgrppropd  13576  mndpropd  13603  imasmnd  13616  grpsubpropd2  13768  imasgrp  13778  subg0  13847  issubg2m  13856  ghmrn  13924  0ghm  13925  resghm2  13928  ghmco  13931  rngpropd  14049  imasrng  14050  srgpcomp  14084  srgpcompp  14085  srgpcomppsc  14086  ringpropd  14132  imasring  14158  qusring2  14160  mulgass3  14179  rhmopp  14271  lringuplu  14291  aprcotr  14381  lmodprop2d  14444  islssmd  14455  2idl0  14608  2idl1  14609  qus2idrng  14621  qus1  14622  qusrhm  14624  znf1o  14747  psrbaglesuppg  14768  psr0cl  14782  psrnegcl  14784  psr1clfi  14789  mplsubgfilemm  14799  lmtopcnp  15061  txopn  15076  blpnfctr  15250  metcnpi  15326  metcnpi2  15327  cncfmpt2fcntop  15410  limcimolemlt  15475  cnplimclemr  15480  limccnp2lem  15487  limccnp2cntop  15488  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvcnp2cntop  15510  dvcn  15511  dvaddxxbr  15512  dvmulxxbr  15513  dvef  15538  lgseisenlem3  15891  lgseisenlem4  15892  iedgedgg  16002  upgrex  16044  upgr1eopdc  16064  upgr1een  16065  umgr1een  16066  usgredg3  16155  uspgr1eopdc  16184  usgr1eop  16186  vtxdfifiun  16238  1loopgruspgr  16244  1loopgrvd2fi  16246  1loopgrvd0fi  16247  1hevtxdg0fi  16248  1hevtxdg1en  16249  1hegrvtxdg1fi  16250  edginwlkd  16296  wlkres  16320  trlsegvdegfi  16408  eupth2lem3lem1fi  16409  eupth2lem3lem2fi  16410  eupth2lem3lem6fi  16412  eupth2lem3lem4fi  16414