Theorem eqsstrrd 3950

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 2745	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3949	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  3sstr3d  3969  ssxpb  6125  fnsnr  7107  suppssof1  8139  oaword1  8477  omword2  8499  oeeui  8528  nnaword1  8555  naddword1  8617  naddunif  8619  cantnfle  9583  cantnflem1d  9600  r1val1  9701  rankr1id  9777  rankxplim3  9796  ackbij2  10155  ttukeylem7  10428  gruima  10716  hashdmpropge2  14436  rlimi  15466  rlimi2  15467  lo1bdd  15473  o1bdd  15484  rlimuni  15503  rlimcld2  15531  o1co  15539  rlimcn1  15541  rlimcn3  15543  o1add2  15577  o1mul2  15578  o1sub2  15579  lo1add  15580  lo1mul  15581  o1dif  15583  rlimneg  15600  rlimsqzlem  15602  lo1le  15605  rlimno1  15607  ramub1lem1  16988  imasaddfnlem  17483  imasvscafn  17492  mrcidb  17572  mrieqv2d  17596  mreexexlem4d  17604  funcres  17854  funcsetcres2  18051  acsfiindd  18510  tsrdir  18561  resmgmhm2  18671  resmhm2  18780  ghmqusnsg  19248  ghmquskerlem3  19252  ghmqusker  19253  f1omvdco2  19414  sylow2a  19585  sylow3lem6  19598  dprdspan  19995  dprd2dlem2  20008  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  dprdsplit  20016  dpjcntz  20020  ablfac1eu  20041  ringidss  20249  subrg1  20554  subrgdvds  20558  subrguss  20559  subrginv  20560  drngdomn  20721  subdrgint  20775  primefld  20777  islss3  20949  lspsnneg  20996  lspextmo  21046  lspsnvs  21107  lsmcv  21134  islbs3  21148  rhmqusnsg  21278  f1lindf  21797  psrbaglesupp  21897  resspsrbas  21948  resspsradd  21949  resspsrmul  21950  evlseu  22059  evlsvvval  22069  epttop  22992  neitr  23163  ordtbas  23175  ordtrest2  23187  pnfnei  23203  mnfnei  23204  ordtrestixx  23205  dnsconst  23361  cmpcld  23385  txindis  23617  txtube  23623  xkohaus  23636  xkopt  23638  xkococnlem  23642  xkoinjcn  23670  qtopval2  23679  ssufl  23901  ufldom  23945  cnextcn  24050  tmdgsum2  24079  clssubg  24092  clsnsg  24093  ustund  24205  ustneism  24207  trust  24212  fmucnd  24274  imasdsf1olem  24356  setsmstopn  24461  metequiv2  24493  metust  24541  restmetu  24553  tngtopn  24633  xlebnum  24950  pi1xfrcnv  25042  limcdif  25861  limccnp  25876  limccnp2  25877  limcco  25878  dvn2bss  25915  cpnord  25920  dvcmulf  25930  dvmptres2  25947  dvmptcmul  25949  dvmptntr  25956  dvcnvrelem2  26003  dvcnvre  26004  taylthlem1  26356  taylthlem2  26357  ulmdvlem3  26385  psercnlem2  26407  rlimcxp  26955  o1cxp  26956  nosupbnd2lem1  27697  noinfbnd2lem1  27712  noetainflem4  27722  bdayiun  27925  negbday  28067  bdaypw2n0bndlem  28473  bdaypw2bnd  28475  bdayfinbndlem1  28477  sspg  30817  ssps  30819  sspn  30825  mdslj1i  32408  mdslj2i  32409  sh1dle  32440  shatomistici  32450  sumdmdii  32504  prssad  32617  prssbd  32618  unidifsnel  32623  tpssad  32627  fisuppov1  32775  resf1o  32822  gsumpart  33144  gsumhashmul  33148  symgcom2  33165  submarchi  33267  nsgmgc  33495  lmhmqusker  33500  rhmquskerlem  33508  idlinsubrg  33514  ressply1evls1  33648  esplyind  33759  ply1degltdimlem  33806  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  extdg1id  33850  fldextrspunlem1  33859  madjusmdetlem1  34011  txomap  34018  rspectopn  34051  zarclssn  34057  zarcmplem  34065  cnvordtrestixx  34097  dya2iocucvr  34468  carsggect  34502  bnj1241  34989  bnj906  35112  fineqvac  35297  cvmscld  35501  fvline2  36374  cldregopn  36559  ttcwf2  36753  pibt2  37779  poimirlem15  38002  sstotbnd2  38141  totbndbnd  38156  heibor1  38177  heiborlem8  38185  lsmsat  39500  lssats  39504  lkrpssN  39655  dia2dimlem5  41560  cdlemn2a  41688  dihglblem6  41832  dochocsp  41871  dochdmj1  41882  dochsatshpb  41944  lcfl9a  41997  lclkrlem2r  42016  lclkrlem2s  42017  lclkrlem2v  42020  lcfrlem6  42039  lcfrlem25  42059  lcfrlem35  42069  mapdval2N  42122  mapdin  42154  baerlem5alem2  42203  baerlem5blem2  42204  evlsbagval  43036  evlsmhpvvval  43045  mhphf  43047  dnnumch2  43490  oege1  43751  omabs2  43777  nadd2rabex  43831  clrellem  44066  iunrelexpmin1  44152  iunrelexpmin2  44156  dftrcl3  44164  brtrclfv2  44171  dfrtrcl3  44177  mnuprdlem1  44716  mnuprdlem2  44717  mullimc  46061  islptre  46064  mullimcf  46068  limcmptdm  46078  dvresntr  46361  itgperiod  46424  fourierdlem89  46638  fourierdlem91  46640  iccpartgt  47902  clnbgrgrim  48425  setrecsres  50192