Theorem eqsstr3d 3412

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

Syntax hints:   -> wi 4   = wceq 1369   C_ wss 3349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363

This theorem is referenced by:  ssxpb  5293  fnsnb  5919  suppssof1OLD  6360  suppssof1  6743  oaword1  7012  omword2  7034  oeeui  7062  nnaword1  7089  cantnfle  7900  cantnflem1d  7917  cantnfleOLD  7930  cantnflem1dOLD  7940  r1val1  8014  rankr1id  8090  rankxplim3  8109  ackbij2  8433  ttukeylem7  8705  gruima  8990  rlimi  13012  rlimi2  13013  lo1bdd  13019  o1bdd  13030  rlimuni  13049  rlimcld2  13077  o1co  13085  rlimcn1  13087  rlimcn2  13089  o1add2  13122  o1mul2  13123  o1sub2  13124  lo1add  13125  lo1mul  13126  o1dif  13128  rlimneg  13145  rlimsqzlem  13147  lo1le  13150  rlimno1  13152  ramub1lem1  14108  imasaddfnlem  14487  imasvscafn  14496  mrcidb  14574  mrieqv2d  14598  mreexexlem4d  14606  funcres  14827  funcsetcres2  14982  acsfiindd  15368  tsrdir  15429  resmhm2  15509  f1omvdco2  15975  sylow2a  16139  sylow3lem6  16152  dprdspan  16546  dprd2dlem2  16561  dprd2dlem1  16562  dprd2da  16563  dmdprdsplit2lem  16566  dprdsplit  16569  dpjcntz  16573  ablfac1eu  16596  rngidss  16693  subrg1  16897  subrgdvds  16901  subrguss  16902  subrginv  16903  islss3  17062  lspsnneg  17109  lspextmo  17159  lspsnvs  17217  lsmcv  17244  islbs3  17258  drngdomn  17397  psrbaglesupp  17457  psrbaglesuppOLD  17458  psrbasOLD  17471  psrlidmOLD  17497  psrridmOLD  17499  resspsrbas  17509  resspsradd  17510  resspsrmul  17511  evlseu  17624  f1lindf  18273  epttop  18635  neitr  18806  ordtbas  18818  ordtrest2  18830  pnfnei  18846  mnfnei  18847  ordtrestixx  18848  dnsconst  19004  cmpcld  19027  txindis  19229  txtube  19235  xkohaus  19248  xkopt  19250  xkococnlem  19254  xkoinjcn  19282  qtopval2  19291  ssufl  19513  ufldom  19557  cnextcn  19661  tmdgsum2  19689  clssubg  19701  clsnsg  19702  ustund  19818  ustneism  19820  trust  19826  fmucnd  19889  imasdsf1olem  19970  setsmstopn  20075  metequiv2  20107  metustOLD  20164  metust  20165  restmetu  20184  tngtopn  20258  xlebnum  20559  pi1xfrcnv  20651  limcdif  21373  limccnp  21388  limccnp2  21389  limcco  21390  dvn2bss  21426  cpnord  21431  dvcmulf  21441  dvmptres2  21458  dvmptcmul  21460  dvmptntr  21467  dvcnvrelem2  21512  dvcnvre  21513  taylthlem1  21860  taylthlem2  21861  ulmdvlem3  21889  psercnlem2  21911  rlimcxp  22389  o1cxp  22390  nbgrassovt  23368  sspg  24148  ssps  24150  sspn  24156  mdslj1i  25745  mdslj2i  25746  sh1dle  25777  shatomistici  25787  sumdmdii  25841  resf1o  26052  submarchi  26225  cnvordtrestixx  26365  ordtrest2NEW  26375  dya2iocucvr  26721  cvmscld  27184  nofulllem3  27867  fvline2  28199  cldregopn  28552  sstotbnd2  28699  totbndbnd  28714  heibor1  28735  heiborlem8  28743  dnnumch2  29424  bnj142OLD  31813  bnj1241  31897  bnj906  32019  lsmsat  32749  lssats  32753  lkrpssN  32904  dia2dimlem5  34809  cdlemn2a  34937  dihglblem6  35081  dochocsp  35120  dochdmj1  35131  dochsatshpb  35193  lcfl9a  35246  lclkrlem2r  35265  lclkrlem2s  35266  lclkrlem2v  35269  lcfrlem6  35288  lcfrlem25  35308  lcfrlem35  35318  mapdval2N  35371  mapdin  35403  baerlem5alem2  35452  baerlem5blem2  35453