Theorem eqsstr3d 3524

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

Syntax hints:   -> wi 4   = wceq 1398   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475

This theorem is referenced by:  ssxpb  5426  fnsnb  6066  suppssof1OLD  6532  suppssof1  6925  oaword1  7193  omword2  7215  oeeui  7243  nnaword1  7270  cantnfle  8081  cantnflem1d  8098  cantnfleOLD  8111  cantnflem1dOLD  8121  r1val1  8195  rankr1id  8271  rankxplim3  8290  ackbij2  8614  ttukeylem7  8886  gruima  9169  rlimi  13418  rlimi2  13419  lo1bdd  13425  o1bdd  13436  rlimuni  13455  rlimcld2  13483  o1co  13491  rlimcn1  13493  rlimcn2  13495  o1add2  13528  o1mul2  13529  o1sub2  13530  lo1add  13531  lo1mul  13532  o1dif  13534  rlimneg  13551  rlimsqzlem  13553  lo1le  13556  rlimno1  13558  ramub1lem1  14628  imasaddfnlem  15017  imasvscafn  15026  mrcidb  15104  mrieqv2d  15128  mreexexlem4d  15136  funcres  15384  funcsetcres2  15571  acsfiindd  16006  tsrdir  16067  resmhm2  16190  f1omvdco2  16672  sylow2a  16838  sylow3lem6  16851  dprdspan  17269  dprd2dlem2  17284  dprd2dlem1  17285  dprd2da  17286  dmdprdsplit2lem  17289  dprdsplit  17292  dpjcntz  17296  ablfac1eu  17319  ringidss  17420  subrg1  17634  subrgdvds  17638  subrguss  17639  subrginv  17640  islss3  17800  lspsnneg  17847  lspextmo  17897  lspsnvs  17955  lsmcv  17982  islbs3  17996  drngdomn  18147  psrbaglesupp  18212  psrbaglesuppOLD  18213  psrbasOLD  18226  psrlidmOLD  18252  psrridmOLD  18254  resspsrbas  18265  resspsradd  18266  resspsrmul  18267  evlseu  18380  f1lindf  19024  epttop  19677  neitr  19848  ordtbas  19860  ordtrest2  19872  pnfnei  19888  mnfnei  19889  ordtrestixx  19890  dnsconst  20046  cmpcld  20069  txindis  20301  txtube  20307  xkohaus  20320  xkopt  20322  xkococnlem  20326  xkoinjcn  20354  qtopval2  20363  ssufl  20585  ufldom  20629  cnextcn  20733  tmdgsum2  20761  clssubg  20773  clsnsg  20774  ustund  20890  ustneism  20892  trust  20898  fmucnd  20961  imasdsf1olem  21042  setsmstopn  21147  metequiv2  21179  metustOLD  21236  metust  21237  restmetu  21256  tngtopn  21330  xlebnum  21631  pi1xfrcnv  21723  limcdif  22446  limccnp  22461  limccnp2  22462  limcco  22463  dvn2bss  22499  cpnord  22504  dvcmulf  22514  dvmptres2  22531  dvmptcmul  22533  dvmptntr  22540  dvcnvrelem2  22585  dvcnvre  22586  taylthlem1  22934  taylthlem2  22935  ulmdvlem3  22963  psercnlem2  22985  rlimcxp  23501  o1cxp  23502  nbgrassovt  24637  sspg  25839  ssps  25841  sspn  25847  mdslj1i  27436  mdslj2i  27437  sh1dle  27468  shatomistici  27478  sumdmdii  27532  resf1o  27784  submarchi  27964  txomap  28072  cnvordtrestixx  28130  dya2iocucvr  28492  carsggect  28526  cvmscld  28982  nofulllem3  29704  fvline2  30024  cldregopn  30389  sstotbnd2  30510  totbndbnd  30525  heibor1  30546  heiborlem8  30554  dnnumch2  31230  mullimc  31861  islptre  31864  mullimcf  31868  limcmptdm  31880  dvresntr  31952  itgperiod  32019  fourierdlem89  32217  fourierdlem91  32219  resmgmhm2  32859  bnj142OLD  34182  bnj1241  34267  bnj906  34389  lsmsat  35130  lssats  35134  lkrpssN  35285  dia2dimlem5  37192  cdlemn2a  37320  dihglblem6  37464  dochocsp  37503  dochdmj1  37514  dochsatshpb  37576  lcfl9a  37629  lclkrlem2r  37648  lclkrlem2s  37649  lclkrlem2v  37652  lcfrlem6  37671  lcfrlem25  37691  lcfrlem35  37701  mapdval2N  37754  mapdin  37786  baerlem5alem2  37835  baerlem5blem2  37836  iunrelexpmin1  38207  iunrelexpmin2  38208  dftrcl3  38213  dfrtrcl3  38214