Theorem eqsstr3d 3379

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

Syntax hints:   -> wi 4   = wceq 1362   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330

This theorem is referenced by:  ssxpb  5260  fnsnb  5885  suppssof1OLD  6328  suppssof1  6711  oaword1  6979  omword2  7001  oeeui  7029  nnaword1  7056  cantnfle  7867  cantnflem1d  7884  cantnfleOLD  7897  cantnflem1dOLD  7907  r1val1  7981  rankr1id  8057  rankxplim3  8076  ackbij2  8400  ttukeylem7  8672  gruima  8956  rlimi  12974  rlimi2  12975  lo1bdd  12981  o1bdd  12992  rlimuni  13011  rlimcld2  13039  o1co  13047  rlimcn1  13049  rlimcn2  13051  o1add2  13084  o1mul2  13085  o1sub2  13086  lo1add  13087  lo1mul  13088  o1dif  13090  rlimneg  13107  rlimsqzlem  13109  lo1le  13112  rlimno1  13114  ramub1lem1  14069  imasaddfnlem  14448  imasvscafn  14457  mrcidb  14535  mrieqv2d  14559  mreexexlem4d  14567  funcres  14788  funcsetcres2  14943  acsfiindd  15329  tsrdir  15390  resmhm2  15469  f1omvdco2  15933  sylow2a  16097  sylow3lem6  16110  dprdspan  16497  dprd2dlem2  16512  dprd2dlem1  16513  dprd2da  16514  dmdprdsplit2lem  16517  dprdsplit  16520  dpjcntz  16524  ablfac1eu  16547  rngidss  16606  subrg1  16798  subrgdvds  16802  subrguss  16803  subrginv  16804  islss3  16961  lspsnneg  17008  lspextmo  17058  lspsnvs  17116  lsmcv  17143  islbs3  17157  drngdomn  17296  psrbaglesupp  17368  psrbaglesuppOLD  17369  psrbasOLD  17382  psrlidmOLD  17408  psrridmOLD  17410  resspsrbas  17420  resspsradd  17421  resspsrmul  17422  f1lindf  18092  epttop  18454  neitr  18625  ordtbas  18637  ordtrest2  18649  pnfnei  18665  mnfnei  18666  ordtrestixx  18667  dnsconst  18823  cmpcld  18846  txindis  19048  txtube  19054  xkohaus  19067  xkopt  19069  xkococnlem  19073  xkoinjcn  19101  qtopval2  19110  ssufl  19332  ufldom  19376  cnextcn  19480  tmdgsum2  19508  clssubg  19520  clsnsg  19521  ustund  19637  ustneism  19639  trust  19645  fmucnd  19708  imasdsf1olem  19789  setsmstopn  19894  metequiv2  19926  metustOLD  19983  metust  19984  restmetu  20003  tngtopn  20077  xlebnum  20378  pi1xfrcnv  20470  limcdif  21192  limccnp  21207  limccnp2  21208  limcco  21209  dvn2bss  21245  cpnord  21250  dvcmulf  21260  dvmptres2  21277  dvmptcmul  21279  dvmptntr  21286  dvcnvrelem2  21331  dvcnvre  21332  evlseu  21367  taylthlem1  21722  taylthlem2  21723  ulmdvlem3  21751  psercnlem2  21773  rlimcxp  22251  o1cxp  22252  nbgrassovt  23168  sspg  23948  ssps  23950  sspn  23956  mdslj1i  25545  mdslj2i  25546  sh1dle  25577  shatomistici  25587  sumdmdii  25641  resf1o  25854  submarchi  26026  cnvordtrestixx  26196  ordtrest2NEW  26206  dya2iocucvr  26552  cvmscld  27009  nofulllem3  27691  fvline2  28023  cldregopn  28367  sstotbnd2  28514  totbndbnd  28529  heibor1  28550  heiborlem8  28558  dnnumch2  29240  bnj142OLD  31416  bnj1241  31500  bnj906  31622  lsmsat  32223  lssats  32227  lkrpssN  32378  dia2dimlem5  34283  cdlemn2a  34411  dihglblem6  34555  dochocsp  34594  dochdmj1  34605  dochsatshpb  34667  lcfl9a  34720  lclkrlem2r  34739  lclkrlem2s  34740  lclkrlem2v  34743  lcfrlem6  34762  lcfrlem25  34782  lcfrlem35  34792  mapdval2N  34845  mapdin  34877  baerlem5alem2  34926  baerlem5blem2  34927