Theorem eqsstr3d 3496

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

Syntax hints:   -> wi 4   = wceq 1437   C_ wss 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447

This theorem is referenced by:  ssxpb  5282  fnsnb  6089  suppssof1  6950  oaword1  7252  omword2  7274  oeeui  7302  nnaword1  7329  cantnfle  8166  cantnflem1d  8183  r1val1  8247  rankr1id  8323  rankxplim3  8342  ackbij2  8662  ttukeylem7  8934  gruima  9216  rlimi  13544  rlimi2  13545  lo1bdd  13551  o1bdd  13562  rlimuni  13581  rlimcld2  13609  o1co  13617  rlimcn1  13619  rlimcn2  13621  o1add2  13654  o1mul2  13655  o1sub2  13656  lo1add  13657  lo1mul  13658  o1dif  13660  rlimneg  13677  rlimsqzlem  13679  lo1le  13682  rlimno1  13684  ramub1lem1  14936  imasaddfnlem  15378  imasvscafn  15387  mrcidb  15465  mrieqv2d  15489  mreexexlem4d  15497  funcres  15745  funcsetcres2  15932  acsfiindd  16367  tsrdir  16428  resmhm2  16551  f1omvdco2  17033  sylow2a  17199  sylow3lem6  17212  dprdspan  17588  dprd2dlem2  17601  dprd2dlem1  17602  dprd2da  17603  dmdprdsplit2lem  17606  dprdsplit  17609  dpjcntz  17613  ablfac1eu  17634  ringidss  17735  subrg1  17946  subrgdvds  17950  subrguss  17951  subrginv  17952  islss3  18110  lspsnneg  18157  lspextmo  18207  lspsnvs  18265  lsmcv  18292  islbs3  18306  drngdomn  18455  psrbaglesupp  18520  resspsrbas  18567  resspsradd  18568  resspsrmul  18569  evlseu  18667  f1lindf  19304  epttop  19948  neitr  20120  ordtbas  20132  ordtrest2  20144  pnfnei  20160  mnfnei  20161  ordtrestixx  20162  dnsconst  20318  cmpcld  20341  txindis  20573  txtube  20579  xkohaus  20592  xkopt  20594  xkococnlem  20598  xkoinjcn  20626  qtopval2  20635  ssufl  20857  ufldom  20901  cnextcn  21006  tmdgsum2  21035  clssubg  21047  clsnsg  21048  ustund  21160  ustneism  21162  trust  21168  fmucnd  21231  imasdsf1olem  21312  setsmstopn  21417  metequiv2  21449  metust  21497  restmetu  21509  tngtopn  21582  xlebnum  21882  pi1xfrcnv  21974  limcdif  22705  limccnp  22720  limccnp2  22721  limcco  22722  dvn2bss  22758  cpnord  22763  dvcmulf  22773  dvmptres2  22790  dvmptcmul  22792  dvmptntr  22799  dvcnvrelem2  22844  dvcnvre  22845  taylthlem1  23190  taylthlem2  23191  ulmdvlem3  23219  psercnlem2  23241  rlimcxp  23761  o1cxp  23762  nbgrassovt  25005  sspg  26209  ssps  26211  sspn  26217  mdslj1i  27804  mdslj2i  27805  sh1dle  27836  shatomistici  27846  sumdmdii  27900  resf1o  28155  submarchi  28338  madjusmdetlem1  28489  txomap  28497  cnvordtrestixx  28555  dya2iocucvr  28942  carsggect  28976  bnj142OLD  29319  bnj1241  29404  bnj906  29526  cvmscld  29781  nofulllem3  30375  fvline2  30695  cldregopn  30769  poimirlem15  31659  sstotbnd2  31810  totbndbnd  31825  heibor1  31846  heiborlem8  31854  lsmsat  32283  lssats  32287  lkrpssN  32438  dia2dimlem5  34345  cdlemn2a  34473  dihglblem6  34617  dochocsp  34656  dochdmj1  34667  dochsatshpb  34729  lcfl9a  34782  lclkrlem2r  34801  lclkrlem2s  34802  lclkrlem2v  34805  lcfrlem6  34824  lcfrlem25  34844  lcfrlem35  34854  mapdval2N  34907  mapdin  34939  baerlem5alem2  34988  baerlem5blem2  34989  dnnumch2  35613  iunrelexpmin1  35943  iunrelexpmin2  35947  dftrcl3  35955  brtrclfv2  35962  dfrtrcl3  35968  mullimc  37272  islptre  37275  mullimcf  37279  limcmptdm  37291  dvresntr  37364  itgperiod  37431  fourierdlem89  37631  fourierdlem91  37633  iccpartgt  38144  resmgmhm2  38570