Theorem eqsstr3d 3453

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

Syntax hints:   -> wi 4   = wceq 1452   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  ssxpb  5277  fnsnb  6099  suppssof1  6967  oaword1  7271  omword2  7293  oeeui  7321  nnaword1  7348  cantnfle  8194  cantnflem1d  8211  r1val1  8275  rankr1id  8351  rankxplim3  8370  ackbij2  8691  ttukeylem7  8963  gruima  9245  rlimi  13654  rlimi2  13655  lo1bdd  13661  o1bdd  13672  rlimuni  13691  rlimcld2  13719  o1co  13727  rlimcn1  13729  rlimcn2  13731  o1add2  13764  o1mul2  13765  o1sub2  13766  lo1add  13767  lo1mul  13768  o1dif  13770  rlimneg  13787  rlimsqzlem  13789  lo1le  13792  rlimno1  13794  ramub1lem1  15063  imasaddfnlem  15512  imasvscafn  15521  mrcidb  15599  mrieqv2d  15623  mreexexlem4d  15631  funcres  15879  funcsetcres2  16066  acsfiindd  16501  tsrdir  16562  resmhm2  16685  f1omvdco2  17167  sylow2a  17349  sylow3lem6  17362  dprdspan  17738  dprd2dlem2  17751  dprd2dlem1  17752  dprd2da  17753  dmdprdsplit2lem  17756  dprdsplit  17759  dpjcntz  17763  ablfac1eu  17784  ringidss  17885  subrg1  18096  subrgdvds  18100  subrguss  18101  subrginv  18102  islss3  18260  lspsnneg  18307  lspextmo  18357  lspsnvs  18415  lsmcv  18442  islbs3  18456  drngdomn  18604  psrbaglesupp  18669  resspsrbas  18716  resspsradd  18717  resspsrmul  18718  evlseu  18816  f1lindf  19457  epttop  20101  neitr  20273  ordtbas  20285  ordtrest2  20297  pnfnei  20313  mnfnei  20314  ordtrestixx  20315  dnsconst  20471  cmpcld  20494  txindis  20726  txtube  20732  xkohaus  20745  xkopt  20747  xkococnlem  20751  xkoinjcn  20779  qtopval2  20788  ssufl  21011  ufldom  21055  cnextcn  21160  tmdgsum2  21189  clssubg  21201  clsnsg  21202  ustund  21314  ustneism  21316  trust  21322  fmucnd  21385  imasdsf1olem  21466  setsmstopn  21571  metequiv2  21603  metust  21651  restmetu  21663  tngtopn  21736  xlebnum  22074  pi1xfrcnv  22166  limcdif  22910  limccnp  22925  limccnp2  22926  limcco  22927  dvn2bss  22963  cpnord  22968  dvcmulf  22978  dvmptres2  22995  dvmptcmul  22997  dvmptntr  23004  dvcnvrelem2  23049  dvcnvre  23050  taylthlem1  23407  taylthlem2  23408  ulmdvlem3  23436  psercnlem2  23458  rlimcxp  23978  o1cxp  23979  nbgrassovt  25242  sspg  26448  ssps  26450  sspn  26456  mdslj1i  28053  mdslj2i  28054  sh1dle  28085  shatomistici  28095  sumdmdii  28149  resf1o  28390  submarchi  28577  madjusmdetlem1  28727  txomap  28735  cnvordtrestixx  28793  dya2iocucvr  29179  carsggect  29223  bnj142OLD  29606  bnj1241  29691  bnj906  29813  cvmscld  30068  nofulllem3  30664  fvline2  30984  cldregopn  31058  poimirlem15  32019  sstotbnd2  32170  totbndbnd  32185  heibor1  32206  heiborlem8  32214  lsmsat  32645  lssats  32649  lkrpssN  32800  dia2dimlem5  34707  cdlemn2a  34835  dihglblem6  34979  dochocsp  35018  dochdmj1  35029  dochsatshpb  35091  lcfl9a  35144  lclkrlem2r  35163  lclkrlem2s  35164  lclkrlem2v  35167  lcfrlem6  35186  lcfrlem25  35206  lcfrlem35  35216  mapdval2N  35269  mapdin  35301  baerlem5alem2  35350  baerlem5blem2  35351  dnnumch2  35974  clrellem  36300  iunrelexpmin1  36371  iunrelexpmin2  36375  dftrcl3  36383  brtrclfv2  36390  dfrtrcl3  36396  mullimc  37793  islptre  37796  mullimcf  37800  limcmptdm  37812  dvresntr  37885  itgperiod  37955  fourierdlem89  38171  fourierdlem91  38173  iccpartgt  38886  structgrssvtxlem  39278  uspgrupgrushgr  39425  resmgmhm2  40307