Theorem eqsstr3d 3539

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 2475	. 2 |- ( ph -> A = B )
3		eqsstr3d.2	. 2 |- ( ph -> B C_ C )
4	2, 3	eqsstrd 3538	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  ssxpb  5441  fnsnb  6080  suppssof1OLD  6543  suppssof1  6933  oaword1  7201  omword2  7223  oeeui  7251  nnaword1  7278  cantnfle  8090  cantnflem1d  8107  cantnfleOLD  8120  cantnflem1dOLD  8130  r1val1  8204  rankr1id  8280  rankxplim3  8299  ackbij2  8623  ttukeylem7  8895  gruima  9180  rlimi  13299  rlimi2  13300  lo1bdd  13306  o1bdd  13317  rlimuni  13336  rlimcld2  13364  o1co  13372  rlimcn1  13374  rlimcn2  13376  o1add2  13409  o1mul2  13410  o1sub2  13411  lo1add  13412  lo1mul  13413  o1dif  13415  rlimneg  13432  rlimsqzlem  13434  lo1le  13437  rlimno1  13439  ramub1lem1  14403  imasaddfnlem  14783  imasvscafn  14792  mrcidb  14870  mrieqv2d  14894  mreexexlem4d  14902  funcres  15123  funcsetcres2  15278  acsfiindd  15664  tsrdir  15725  resmhm2  15810  f1omvdco2  16279  sylow2a  16445  sylow3lem6  16458  dprdspan  16876  dprd2dlem2  16891  dprd2dlem1  16892  dprd2da  16893  dmdprdsplit2lem  16896  dprdsplit  16899  dpjcntz  16903  ablfac1eu  16926  rngidss  17026  subrg1  17239  subrgdvds  17243  subrguss  17244  subrginv  17245  islss3  17405  lspsnneg  17452  lspextmo  17502  lspsnvs  17560  lsmcv  17587  islbs3  17601  drngdomn  17751  psrbaglesupp  17816  psrbaglesuppOLD  17817  psrbasOLD  17830  psrlidmOLD  17856  psrridmOLD  17858  resspsrbas  17869  resspsradd  17870  resspsrmul  17871  evlseu  17984  f1lindf  18652  epttop  19304  neitr  19475  ordtbas  19487  ordtrest2  19499  pnfnei  19515  mnfnei  19516  ordtrestixx  19517  dnsconst  19673  cmpcld  19696  txindis  19898  txtube  19904  xkohaus  19917  xkopt  19919  xkococnlem  19923  xkoinjcn  19951  qtopval2  19960  ssufl  20182  ufldom  20226  cnextcn  20330  tmdgsum2  20358  clssubg  20370  clsnsg  20371  ustund  20487  ustneism  20489  trust  20495  fmucnd  20558  imasdsf1olem  20639  setsmstopn  20744  metequiv2  20776  metustOLD  20833  metust  20834  restmetu  20853  tngtopn  20927  xlebnum  21228  pi1xfrcnv  21320  limcdif  22043  limccnp  22058  limccnp2  22059  limcco  22060  dvn2bss  22096  cpnord  22101  dvcmulf  22111  dvmptres2  22128  dvmptcmul  22130  dvmptntr  22137  dvcnvrelem2  22182  dvcnvre  22183  taylthlem1  22530  taylthlem2  22531  ulmdvlem3  22559  psercnlem2  22581  rlimcxp  23059  o1cxp  23060  nbgrassovt  24139  sspg  25345  ssps  25347  sspn  25353  mdslj1i  26942  mdslj2i  26943  sh1dle  26974  shatomistici  26984  sumdmdii  27038  resf1o  27253  submarchi  27420  txomap  27528  cnvordtrestixx  27559  ordtrest2NEW  27569  dya2iocucvr  27923  cvmscld  28386  nofulllem3  29069  fvline2  29401  cldregopn  29754  sstotbnd2  29901  totbndbnd  29916  heibor1  29937  heiborlem8  29945  dnnumch2  30623  mullimc  31186  mullimcf  31193  limcmptdm  31205  dvresntr  31274  itgsubsticclem  31321  itgperiod  31327  fourierdlem49  31484  bnj142OLD  32879  bnj1241  32963  bnj906  33085  lsmsat  33823  lssats  33827  lkrpssN  33978  dia2dimlem5  35883  cdlemn2a  36011  dihglblem6  36155  dochocsp  36194  dochdmj1  36205  dochsatshpb  36267  lcfl9a  36320  lclkrlem2r  36339  lclkrlem2s  36340  lclkrlem2v  36343  lcfrlem6  36362  lcfrlem25  36382  lcfrlem35  36392  mapdval2N  36445  mapdin  36477  baerlem5alem2  36526  baerlem5blem2  36527