Theorem eleqtrrd 2318

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  3eltr4d  2322  rspc2vd  3216  exmidsssnc  4340  funopsn  5891  tfrexlem  6605  nnsucuniel  6768  erref  6827  en1uniel  7091  fin0  7189  fin0or  7190  pw1if  7585  prarloclemarch2  7787  fzopth  10478  fzoss2  10592  fz1fzo0m1  10612  fzo0addel  10617  fzo0addelr  10618  elfzoext  10621  fzosubel3  10625  elfzomin  10635  elfzonlteqm1  10639  fzoend  10651  fzofzp1  10656  fzofzp1b  10657  peano2fzor  10661  zmodfzo  10799  frecuzrdg0  10865  frecuzrdgsuc  10866  frecuzrdgdomlem  10869  frecuzrdg0t  10874  frecuzrdgsuctlem  10875  seq3f1olemqsum  10965  seqf1oglem2  10972  bcn2  11218  ccats1val2  11424  swrdccat2  11459  pfxccat1  11490  swrdswrd  11493  pfxccatin12  11521  summodclem2a  12167  fisumss  12178  fsumm1  12202  fisumcom2  12224  prodmodclem2a  12362  fprodm1  12384  fprodcom2fi  12412  ballotfilemrv  13315  ennnfonelemex  13357  ctinfomlemom  13370  strslfv3  13450  bassetsnn  13461  sgrppropd  13781  mndpropd  13806  imasmnd  13813  grpsubpropd2  13963  imasgrp  13967  subg0  14036  issubg2m  14045  ghmrn  14113  0ghm  14114  resghm2  14117  ghmco  14120  rngpropd  14338  imasrng  14339  srgpcomp  14378  srgpcompp  14379  srgpcomppsc  14380  ringpropd  14427  imasring  14453  qusring2  14455  mulgass3  14475  rhmopp  14567  lringuplu  14587  aprcotr  14681  lmodprop2d  14769  islssmd  14780  2idl0  14933  2idl1  14934  qus2idrng  14946  qus1  14947  qusrhm  14949  znf1o  15070  assapropd  15098  psrbaglesuppg  15141  psrbagaddclfi  15145  psrbaglefifi  15147  psr0cl  15163  psrnegcl  15165  psr1clfi  15170  mplsubgfilemm  15180  lmtopcnp  15442  txopn  15457  blpnfctr  15631  metcnpi  15707  metcnpi2  15708  cncfmpt2fcntop  15791  limcimolemlt  15856  cnplimclemr  15861  limccnp2lem  15868  limccnp2cntop  15869  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvcn  15892  dvaddxxbr  15893  dvmulxxbr  15894  dvef  15919  lgseisenlem3  16357  lgseisenlem4  16358  iedgedgg  16468  upgrex  16510  upgr1eopdc  16530  upgr1een  16531  umgr1een  16532  usgredg3  16621  uspgr1eopdc  16650  usgr1eop  16652  vtxdfifiun  16704  1loopgruspgr  16710  1loopgrvd2fi  16712  1loopgrvd0fi  16713  1hevtxdg0fi  16714  1hevtxdg1en  16715  1hegrvtxdg1fi  16716  edginwlkd  16762  wlkres  16786  trlsegvdegfi  16874  eupth2lem3lem1fi  16875  eupth2lem3lem2fi  16876  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880