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  7584  prarloclemarch2  7786  fzopth  10467  fzoss2  10581  fz1fzo0m1  10601  fzo0addel  10606  fzo0addelr  10607  elfzoext  10610  fzosubel3  10614  elfzomin  10624  elfzonlteqm1  10628  fzoend  10640  fzofzp1  10645  fzofzp1b  10646  peano2fzor  10650  zmodfzo  10784  frecuzrdg0  10850  frecuzrdgsuc  10851  frecuzrdgdomlem  10854  frecuzrdg0t  10859  frecuzrdgsuctlem  10860  seq3f1olemqsum  10950  seqf1oglem2  10957  bcn2  11202  ccats1val2  11408  swrdccat2  11443  pfxccat1  11474  swrdswrd  11477  pfxccatin12  11505  summodclem2a  12148  fisumss  12159  fsumm1  12183  fisumcom2  12205  prodmodclem2a  12343  fprodm1  12365  fprodcom2fi  12393  ballotfilemrv  13263  ennnfonelemex  13305  ctinfomlemom  13318  strslfv3  13398  bassetsnn  13409  sgrppropd  13728  mndpropd  13753  imasmnd  13760  grpsubpropd2  13910  imasgrp  13914  subg0  13983  issubg2m  13992  ghmrn  14060  0ghm  14061  resghm2  14064  ghmco  14067  rngpropd  14254  imasrng  14255  srgpcomp  14294  srgpcompp  14295  srgpcomppsc  14296  ringpropd  14343  imasring  14369  qusring2  14371  mulgass3  14391  rhmopp  14483  lringuplu  14503  aprcotr  14597  lmodprop2d  14685  islssmd  14696  2idl0  14849  2idl1  14850  qus2idrng  14862  qus1  14863  qusrhm  14865  znf1o  14986  assapropd  15014  psrbaglesuppg  15057  psrbagaddclfi  15061  psr0cl  15072  psrnegcl  15074  psr1clfi  15079  mplsubgfilemm  15089  lmtopcnp  15351  txopn  15366  blpnfctr  15540  metcnpi  15616  metcnpi2  15617  cncfmpt2fcntop  15700  limcimolemlt  15765  cnplimclemr  15770  limccnp2lem  15777  limccnp2cntop  15778  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvcn  15801  dvaddxxbr  15802  dvmulxxbr  15803  dvef  15828  lgseisenlem3  16191  lgseisenlem4  16192  iedgedgg  16302  upgrex  16344  upgr1eopdc  16364  upgr1een  16365  umgr1een  16366  usgredg3  16455  uspgr1eopdc  16484  usgr1eop  16486  vtxdfifiun  16538  1loopgruspgr  16544  1loopgrvd2fi  16546  1loopgrvd0fi  16547  1hevtxdg0fi  16548  1hevtxdg1en  16549  1hegrvtxdg1fi  16550  edginwlkd  16596  wlkres  16620  trlsegvdegfi  16708  eupth2lem3lem1fi  16709  eupth2lem3lem2fi  16710  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714