Theorem eqsstrrd 3967

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrrd.1	⊢ (𝜑 → 𝐵 = 𝐴)
eqsstrrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrd

Step	Hyp	Ref	Expression
1		eqsstrrd.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2740	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3966	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916

This theorem is referenced by:  3sstr3d  3986  ssxpb  6130  fnsnr  7107  suppssof1  8139  oaword1  8477  omword2  8499  oeeui  8528  nnaword1  8555  naddword1  8617  naddunif  8619  cantnfle  9578  cantnflem1d  9595  r1val1  9696  rankr1id  9772  rankxplim3  9791  ackbij2  10150  ttukeylem7  10423  gruima  10711  hashdmpropge2  14404  rlimi  15434  rlimi2  15435  lo1bdd  15441  o1bdd  15452  rlimuni  15471  rlimcld2  15499  o1co  15507  rlimcn1  15509  rlimcn3  15511  o1add2  15545  o1mul2  15546  o1sub2  15547  lo1add  15548  lo1mul  15549  o1dif  15551  rlimneg  15568  rlimsqzlem  15570  lo1le  15573  rlimno1  15575  ramub1lem1  16952  imasaddfnlem  17447  imasvscafn  17456  mrcidb  17536  mrieqv2d  17560  mreexexlem4d  17568  funcres  17818  funcsetcres2  18015  acsfiindd  18474  tsrdir  18525  resmgmhm2  18635  resmhm2  18744  ghmqusnsg  19209  ghmquskerlem3  19213  ghmqusker  19214  f1omvdco2  19375  sylow2a  19546  sylow3lem6  19559  dprdspan  19956  dprd2dlem2  19969  dprd2dlem1  19970  dprd2da  19971  dmdprdsplit2lem  19974  dprdsplit  19977  dpjcntz  19981  ablfac1eu  20002  ringidss  20210  subrg1  20513  subrgdvds  20517  subrguss  20518  subrginv  20519  drngdomn  20680  subdrgint  20734  primefld  20736  islss3  20908  lspsnneg  20955  lspextmo  21006  lspsnvs  21067  lsmcv  21094  islbs3  21108  rhmqusnsg  21238  f1lindf  21775  psrbaglesupp  21876  resspsrbas  21927  resspsradd  21928  resspsrmul  21929  evlseu  22036  evlsvvval  22046  epttop  22951  neitr  23122  ordtbas  23134  ordtrest2  23146  pnfnei  23162  mnfnei  23163  ordtrestixx  23164  dnsconst  23320  cmpcld  23344  txindis  23576  txtube  23582  xkohaus  23595  xkopt  23597  xkococnlem  23601  xkoinjcn  23629  qtopval2  23638  ssufl  23860  ufldom  23904  cnextcn  24009  tmdgsum2  24038  clssubg  24051  clsnsg  24052  ustund  24164  ustneism  24166  trust  24171  fmucnd  24233  imasdsf1olem  24315  setsmstopn  24420  metequiv2  24452  metust  24500  restmetu  24512  tngtopn  24592  xlebnum  24918  pi1xfrcnv  25011  limcdif  25831  limccnp  25846  limccnp2  25847  limcco  25848  dvn2bss  25886  cpnord  25891  dvcmulf  25902  dvmptres2  25920  dvmptcmul  25922  dvmptntr  25929  dvcnvrelem2  25977  dvcnvre  25978  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulmdvlem3  26365  psercnlem2  26388  rlimcxp  26938  o1cxp  26939  nosupbnd2lem1  27681  noinfbnd2lem1  27696  noetainflem4  27706  bdayiun  27887  negsbday  28026  bdaypw2n0s  28420  sspg  30752  ssps  30754  sspn  30760  mdslj1i  32343  mdslj2i  32344  sh1dle  32375  shatomistici  32385  sumdmdii  32439  prssad  32553  prssbd  32554  unidifsnel  32559  tpssad  32563  fisuppov1  32711  resf1o  32758  gsumpart  33095  gsumhashmul  33099  symgcom2  33115  submarchi  33217  nsgmgc  33442  lmhmqusker  33447  rhmquskerlem  33455  idlinsubrg  33461  ressply1evls1  33595  esplyind  33680  ply1degltdimlem  33728  fedgmullem1  33735  fedgmullem2  33736  fedgmul  33737  extdg1id  33772  fldextrspunlem1  33781  madjusmdetlem1  33933  txomap  33940  rspectopn  33973  zarclssn  33979  zarcmplem  33987  cnvordtrestixx  34019  dya2iocucvr  34390  carsggect  34424  bnj1241  34912  bnj906  35035  fineqvac  35221  cvmscld  35416  fvline2  36289  cldregopn  36474  pibt2  37561  poimirlem15  37775  sstotbnd2  37914  totbndbnd  37929  heibor1  37950  heiborlem8  37958  lsmsat  39207  lssats  39211  lkrpssN  39362  dia2dimlem5  41267  cdlemn2a  41395  dihglblem6  41539  dochocsp  41578  dochdmj1  41589  dochsatshpb  41651  lcfl9a  41704  lclkrlem2r  41723  lclkrlem2s  41724  lclkrlem2v  41727  lcfrlem6  41746  lcfrlem25  41766  lcfrlem35  41776  mapdval2N  41829  mapdin  41861  baerlem5alem2  41910  baerlem5blem2  41911  evlsbagval  42754  evlsmhpvvval  42780  mhphf  42782  dnnumch2  43229  oege1  43490  omabs2  43516  nadd2rabex  43570  clrellem  43805  iunrelexpmin1  43891  iunrelexpmin2  43895  dftrcl3  43903  brtrclfv2  43910  dfrtrcl3  43916  mnuprdlem1  44455  mnuprdlem2  44456  mullimc  45804  islptre  45807  mullimcf  45811  limcmptdm  45821  dvresntr  46104  itgperiod  46167  fourierdlem89  46381  fourierdlem91  46383  iccpartgt  47615  clnbgrgrim  48122  setrecsres  49889