Theorem eqsstr3d 3521

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstr3d.1	|- ( ph -> B = A )
eqsstr3d.2	|- ( ph -> B C_ C )

Assertion

Ref	Expression
eqsstr3d	|- ( ph -> A C_ C )

Proof of Theorem eqsstr3d

Step	Hyp	Ref	Expression
1		eqsstr3d.1	. . 3 |- ( ph -> B = A )
2	1	eqcomd 2449	. 2 |- ( ph -> A = B )
3		eqsstr3d.2	. 2 |- ( ph -> B C_ C )
4	2, 3	eqsstrd 3520	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1381   C_ wss 3458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472

This theorem is referenced by:  ssxpb  5427  fnsnb  6071  suppssof1OLD  6540  suppssof1  6931  oaword1  7199  omword2  7221  oeeui  7249  nnaword1  7276  cantnfle  8088  cantnflem1d  8105  cantnfleOLD  8118  cantnflem1dOLD  8128  r1val1  8202  rankr1id  8278  rankxplim3  8297  ackbij2  8621  ttukeylem7  8893  gruima  9178  rlimi  13310  rlimi2  13311  lo1bdd  13317  o1bdd  13328  rlimuni  13347  rlimcld2  13375  o1co  13383  rlimcn1  13385  rlimcn2  13387  o1add2  13420  o1mul2  13421  o1sub2  13422  lo1add  13423  lo1mul  13424  o1dif  13426  rlimneg  13443  rlimsqzlem  13445  lo1le  13448  rlimno1  13450  ramub1lem1  14416  imasaddfnlem  14797  imasvscafn  14806  mrcidb  14884  mrieqv2d  14908  mreexexlem4d  14916  funcres  15134  funcsetcres2  15289  acsfiindd  15676  tsrdir  15737  resmhm2  15860  f1omvdco2  16342  sylow2a  16508  sylow3lem6  16521  dprdspan  16942  dprd2dlem2  16957  dprd2dlem1  16958  dprd2da  16959  dmdprdsplit2lem  16962  dprdsplit  16965  dpjcntz  16969  ablfac1eu  16992  ringidss  17093  subrg1  17307  subrgdvds  17311  subrguss  17312  subrginv  17313  islss3  17473  lspsnneg  17520  lspextmo  17570  lspsnvs  17628  lsmcv  17655  islbs3  17669  drngdomn  17820  psrbaglesupp  17885  psrbaglesuppOLD  17886  psrbasOLD  17899  psrlidmOLD  17925  psrridmOLD  17927  resspsrbas  17938  resspsradd  17939  resspsrmul  17940  evlseu  18053  f1lindf  18724  epttop  19376  neitr  19547  ordtbas  19559  ordtrest2  19571  pnfnei  19587  mnfnei  19588  ordtrestixx  19589  dnsconst  19745  cmpcld  19768  txindis  20001  txtube  20007  xkohaus  20020  xkopt  20022  xkococnlem  20026  xkoinjcn  20054  qtopval2  20063  ssufl  20285  ufldom  20329  cnextcn  20433  tmdgsum2  20461  clssubg  20473  clsnsg  20474  ustund  20590  ustneism  20592  trust  20598  fmucnd  20661  imasdsf1olem  20742  setsmstopn  20847  metequiv2  20879  metustOLD  20936  metust  20937  restmetu  20956  tngtopn  21030  xlebnum  21331  pi1xfrcnv  21423  limcdif  22146  limccnp  22161  limccnp2  22162  limcco  22163  dvn2bss  22199  cpnord  22204  dvcmulf  22214  dvmptres2  22231  dvmptcmul  22233  dvmptntr  22240  dvcnvrelem2  22285  dvcnvre  22286  taylthlem1  22633  taylthlem2  22634  ulmdvlem3  22662  psercnlem2  22684  rlimcxp  23168  o1cxp  23169  nbgrassovt  24300  sspg  25506  ssps  25508  sspn  25514  mdslj1i  27103  mdslj2i  27104  sh1dle  27135  shatomistici  27145  sumdmdii  27199  resf1o  27418  submarchi  27596  txomap  27703  cnvordtrestixx  27761  dya2iocucvr  28121  cvmscld  28584  nofulllem3  29432  fvline2  29764  cldregopn  30117  sstotbnd2  30238  totbndbnd  30253  heibor1  30274  heiborlem8  30282  dnnumch2  30959  mullimc  31526  islptre  31529  mullimcf  31533  limcmptdm  31545  dvresntr  31613  itgperiod  31666  fourierdlem89  31863  fourierdlem91  31865  resmgmhm2  32321  bnj142OLD  33489  bnj1241  33573  bnj906  33695  lsmsat  34435  lssats  34439  lkrpssN  34590  dia2dimlem5  36497  cdlemn2a  36625  dihglblem6  36769  dochocsp  36808  dochdmj1  36819  dochsatshpb  36881  lcfl9a  36934  lclkrlem2r  36953  lclkrlem2s  36954  lclkrlem2v  36957  lcfrlem6  36976  lcfrlem25  36996  lcfrlem35  37006  mapdval2N  37059  mapdin  37091  baerlem5alem2  37140  baerlem5blem2  37141