Theorem eqsstr3d 3343

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

Syntax hints:   -> wi 4   = wceq 1649   C_ wss 3280

This theorem is referenced by:  ssxpb  5262  suppssof1  6305  oaword1  6754  omword2  6776  oeeui  6804  nnaword1  6831  cantnfle  7582  cantnflem1d  7600  r1val1  7668  rankr1id  7744  rankxplim3  7761  ackbij2  8079  ttukeylem7  8351  gruima  8633  rlimi  12262  rlimi2  12263  lo1bdd  12269  o1bdd  12280  rlimuni  12299  rlimcld2  12327  o1co  12335  rlimcn1  12337  rlimcn2  12339  o1add2  12372  o1mul2  12373  o1sub2  12374  lo1add  12375  lo1mul  12376  o1dif  12378  rlimneg  12395  rlimsqzlem  12397  lo1le  12400  rlimno1  12402  ramub1lem1  13349  imasaddfnlem  13708  imasvscafn  13717  mrcidb  13795  mrieqv2d  13819  mreexexlem4d  13827  funcres  14048  funcsetcres2  14203  acsfiindd  14558  tsrdir  14638  resmhm2  14715  sylow2a  15208  sylow3lem6  15221  dprdspan  15540  dprd2dlem2  15553  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  dprdsplit  15561  dpjcntz  15565  ablfac1eu  15586  rngidss  15645  subrg1  15833  subrgdvds  15837  subrguss  15838  subrginv  15839  islss3  15990  lspsnneg  16037  lspextmo  16087  lspsnvs  16141  lsmcv  16168  islbs3  16182  drngdomn  16318  psrbaglesupp  16388  psrbas  16398  psrlidm  16422  psrridm  16423  resspsrbas  16433  resspsradd  16434  resspsrmul  16435  epttop  17028  neitr  17198  ordtbas  17210  ordtrest2  17222  pnfnei  17238  mnfnei  17239  ordtrestixx  17240  dnsconst  17396  cmpcld  17419  txindis  17619  txtube  17625  xkohaus  17638  xkopt  17640  xkococnlem  17644  xkoinjcn  17672  qtopval2  17681  ssufl  17903  ufldom  17947  cnextcn  18051  tmdgsum2  18079  clssubg  18091  clsnsg  18092  ustund  18204  ustneism  18206  trust  18212  fmucnd  18275  imasdsf1olem  18356  setsmstopn  18461  metequiv2  18493  metustOLD  18550  metust  18551  restmetu  18570  tngtopn  18644  xlebnum  18943  pi1xfrcnv  19035  limcdif  19716  limccnp  19731  limccnp2  19732  limcco  19733  dvn2bss  19769  cpnord  19774  dvcmulf  19784  dvmptres2  19801  dvmptcmul  19803  dvmptntr  19810  dvcnvrelem2  19855  dvcnvre  19856  evlseu  19890  taylthlem1  20242  taylthlem2  20243  ulmdvlem3  20271  psercnlem2  20293  rlimcxp  20765  o1cxp  20766  nbgrassovt  21400  sspg  22180  ssps  22182  sspn  22188  mdslj1i  23775  mdslj2i  23776  sh1dle  23807  shatomistici  23817  sumdmdii  23871  cnvordtrestixx  24264  dya2iocucvr  24587  cvmscld  24913  nofulllem3  25572  fvline2  25984  cldregopn  26224  sstotbnd2  26373  totbndbnd  26388  heibor1  26409  heiborlem8  26417  dnnumch2  27010  f1lindf  27160  f1omvdco2  27259  bnj142  28799  bnj1241  28885  bnj906  29007  lsmsat  29491  lssats  29495  lkrpssN  29646  dia2dimlem5  31551  cdlemn2a  31679  dihglblem6  31823  dochocsp  31862  dochdmj1  31873  dochsatshpb  31935  lcfl9a  31988  lclkrlem2r  32007  lclkrlem2s  32008  lclkrlem2v  32011  lcfrlem6  32030  lcfrlem25  32050  lcfrlem35  32060  mapdval2N  32113  mapdin  32145  baerlem5alem2  32194  baerlem5blem2  32195

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294