Theorem eleqtrrd 2309

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  3eltr4d  2313  rspc2vd  3193  exmidsssnc  4287  funopsn  5819  tfrexlem  6486  nnsucuniel  6649  erref  6708  en1uniel  6964  fin0  7055  fin0or  7056  pw1if  7421  prarloclemarch2  7617  fzopth  10269  fzoss2  10382  fz1fzo0m1  10401  fzo0addel  10406  fzo0addelr  10407  elfzoext  10410  fzosubel3  10414  elfzomin  10424  elfzonlteqm1  10428  fzoend  10440  fzofzp1  10445  fzofzp1b  10446  peano2fzor  10450  zmodfzo  10581  frecuzrdg0  10647  frecuzrdgsuc  10648  frecuzrdgdomlem  10651  frecuzrdg0t  10656  frecuzrdgsuctlem  10657  seq3f1olemqsum  10747  seqf1oglem2  10754  bcn2  10998  ccats1val2  11187  swrdccat2  11219  pfxccat1  11250  swrdswrd  11253  pfxccatin12  11281  summodclem2a  11908  fisumss  11919  fsumm1  11943  fisumcom2  11965  prodmodclem2a  12103  fprodm1  12125  fprodcom2fi  12153  ennnfonelemex  13001  ctinfomlemom  13014  strslfv3  13094  bassetsnn  13105  gsumpropd2  13442  sgrppropd  13462  mndpropd  13489  imasmnd  13502  grpsubpropd2  13654  imasgrp  13664  subg0  13733  issubg2m  13742  ghmrn  13810  0ghm  13811  resghm2  13814  ghmco  13817  rngpropd  13934  imasrng  13935  srgpcomp  13969  srgpcompp  13970  srgpcomppsc  13971  ringpropd  14017  imasring  14043  qusring2  14045  mulgass3  14064  rhmopp  14156  lringuplu  14176  aprcotr  14265  lmodprop2d  14328  islssmd  14339  2idl0  14492  2idl1  14493  qus2idrng  14505  qus1  14506  qusrhm  14508  znf1o  14631  psrbaglesuppg  14652  psr0cl  14661  psrnegcl  14663  psr1clfi  14668  mplsubgfilemm  14678  lmtopcnp  14940  txopn  14955  blpnfctr  15129  metcnpi  15205  metcnpi2  15206  cncfmpt2fcntop  15289  limcimolemlt  15354  cnplimclemr  15359  limccnp2lem  15366  limccnp2cntop  15367  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvcnp2cntop  15389  dvcn  15390  dvaddxxbr  15391  dvmulxxbr  15392  dvef  15417  lgseisenlem3  15767  lgseisenlem4  15768  iedgedgg  15877  upgrex  15919  upgr1eopdc  15939  usgredg3  16028  vtxdfifiun  16057  edginwlkd  16101  wlkres  16123