Theorem eqsstr3d 3467

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

Syntax hints:   -> wi 4   = wceq 1444   C_ wss 3404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418

This theorem is referenced by:  ssxpb  5271  fnsnb  6083  suppssof1  6948  oaword1  7253  omword2  7275  oeeui  7303  nnaword1  7330  cantnfle  8176  cantnflem1d  8193  r1val1  8257  rankr1id  8333  rankxplim3  8352  ackbij2  8673  ttukeylem7  8945  gruima  9227  rlimi  13577  rlimi2  13578  lo1bdd  13584  o1bdd  13595  rlimuni  13614  rlimcld2  13642  o1co  13650  rlimcn1  13652  rlimcn2  13654  o1add2  13687  o1mul2  13688  o1sub2  13689  lo1add  13690  lo1mul  13691  o1dif  13693  rlimneg  13710  rlimsqzlem  13712  lo1le  13715  rlimno1  13717  ramub1lem1  14984  imasaddfnlem  15434  imasvscafn  15443  mrcidb  15521  mrieqv2d  15545  mreexexlem4d  15553  funcres  15801  funcsetcres2  15988  acsfiindd  16423  tsrdir  16484  resmhm2  16607  f1omvdco2  17089  sylow2a  17271  sylow3lem6  17284  dprdspan  17660  dprd2dlem2  17673  dprd2dlem1  17674  dprd2da  17675  dmdprdsplit2lem  17678  dprdsplit  17681  dpjcntz  17685  ablfac1eu  17706  ringidss  17807  subrg1  18018  subrgdvds  18022  subrguss  18023  subrginv  18024  islss3  18182  lspsnneg  18229  lspextmo  18279  lspsnvs  18337  lsmcv  18364  islbs3  18378  drngdomn  18527  psrbaglesupp  18592  resspsrbas  18639  resspsradd  18640  resspsrmul  18641  evlseu  18739  f1lindf  19380  epttop  20024  neitr  20196  ordtbas  20208  ordtrest2  20220  pnfnei  20236  mnfnei  20237  ordtrestixx  20238  dnsconst  20394  cmpcld  20417  txindis  20649  txtube  20655  xkohaus  20668  xkopt  20670  xkococnlem  20674  xkoinjcn  20702  qtopval2  20711  ssufl  20933  ufldom  20977  cnextcn  21082  tmdgsum2  21111  clssubg  21123  clsnsg  21124  ustund  21236  ustneism  21238  trust  21244  fmucnd  21307  imasdsf1olem  21388  setsmstopn  21493  metequiv2  21525  metust  21573  restmetu  21585  tngtopn  21658  xlebnum  21996  pi1xfrcnv  22088  limcdif  22831  limccnp  22846  limccnp2  22847  limcco  22848  dvn2bss  22884  cpnord  22889  dvcmulf  22899  dvmptres2  22916  dvmptcmul  22918  dvmptntr  22925  dvcnvrelem2  22970  dvcnvre  22971  taylthlem1  23328  taylthlem2  23329  ulmdvlem3  23357  psercnlem2  23379  rlimcxp  23899  o1cxp  23900  nbgrassovt  25163  sspg  26367  ssps  26369  sspn  26375  mdslj1i  27972  mdslj2i  27973  sh1dle  28004  shatomistici  28014  sumdmdii  28068  resf1o  28315  submarchi  28503  madjusmdetlem1  28653  txomap  28661  cnvordtrestixx  28719  dya2iocucvr  29106  carsggect  29150  bnj142OLD  29534  bnj1241  29619  bnj906  29741  cvmscld  29996  nofulllem3  30593  fvline2  30913  cldregopn  30987  poimirlem15  31955  sstotbnd2  32106  totbndbnd  32121  heibor1  32142  heiborlem8  32150  lsmsat  32574  lssats  32578  lkrpssN  32729  dia2dimlem5  34636  cdlemn2a  34764  dihglblem6  34908  dochocsp  34947  dochdmj1  34958  dochsatshpb  35020  lcfl9a  35073  lclkrlem2r  35092  lclkrlem2s  35093  lclkrlem2v  35096  lcfrlem6  35115  lcfrlem25  35135  lcfrlem35  35145  mapdval2N  35198  mapdin  35230  baerlem5alem2  35279  baerlem5blem2  35280  dnnumch2  35903  clrellem  36229  iunrelexpmin1  36300  iunrelexpmin2  36304  dftrcl3  36312  brtrclfv2  36319  dfrtrcl3  36325  mullimc  37696  islptre  37699  mullimcf  37703  limcmptdm  37715  dvresntr  37788  itgperiod  37858  fourierdlem89  38059  fourierdlem91  38061  iccpartgt  38741  structgrssvtxlem  39125  uspgrupgrushgr  39264  resmgmhm2  39852