Theorem eqsstrdi 3980

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

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

Assertion

Ref	Expression
eqsstrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrdi

Step	Hyp	Ref	Expression
1		eqsstrdi.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqsstrdi.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	1, 3	eqsstrd 3970	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  eqsstrrdi  3981  eqimssd  3992  dmxpss  6157  dmsnopss  6201  iotassuni  6496  fvmptss  6988  fvmptss2  7002  funressn  7142  riotassuni  7393  ordsuci  7791  frxp  8106  suppssdm  8157  suppun  8164  suppss  8174  suppssov1  8177  suppssov2  8178  suppss2  8180  suppssfv  8182  oawordeulem  8523  omwordri  8541  oewordri  8562  mapssfset  8832  fodomr  9100  fodomfir  9272  fipwuni  9372  fipwss  9375  ordtypelem6  9471  inf3lemd  9582  cantnfle  9626  cantnflem2  9645  ttrclselem1  9680  en2other2  9965  ackbij1lem15  10189  ackbij2lem3  10196  cfub  10205  cflecard  10209  cfle  10210  fin23lem13  10289  fin23lem29  10298  compsscnvlem  10327  itunitc1  10377  fpwwe2lem11  10599  grur1a  10777  uzssz  12860  fsuppmapnn0fiublem  14003  fsuppmapnn0fiub  14004  swrdlend  14667  repswswrd  14797  cshimadifsn  14842  xptrrel  14993  relexpnndm  15054  relexpdmd  15057  relexprnd  15061  relexpfldd  15063  rtrclreclem4  15074  limsupgle  15504  isercolllem2  15693  isercolllem3  15694  isercoll  15695  fsumss  15752  sadcaddlem  16491  sadadd2lem  16493  sadadd3  16495  sadcl  16496  sadaddlem  16500  sadasslem  16504  sadeq  16506  smupvallem  16517  smucl  16518  prmreclem4  16955  prmreclem5  16956  1arith  16963  vdwmc2  17015  vdwlem13  17029  ramz2  17060  strfvss  17223  ressbasssg  17273  ressbasssOLD  17276  prdsless  17492  sectss  17785  invss  17794  fullfunc  17941  fthfunc  17942  catccatid  18139  resscatc  18142  catcisolem  18143  catciso  18144  yoniso  18317  gsumpropd2lem  18713  cntzrcl  19367  cntzssv  19368  gsumzmhm  19977  ablfaclem3  20129  rnghmresfn  20665  dfrngc2  20674  rnghmsscmap2  20675  rnghmsscmap  20676  funcrngcsetc  20686  rhmresfn  20694  dfringc2  20703  rhmsscmap2  20704  rhmsscmap  20705  rhmsscrnghm  20711  funcringcsetc  20720  rngcrescrhm  20730  rhmsubclem1  20731  rhmsubclem4  20734  lmhmlsp  21113  evpmss  21635  cssss  21734  frlmplusgval  21813  frlmvscafval  21815  uvcresum  21842  resspsrbas  22022  resspsrvsca  22025  subrgpsr  22026  mplsubglem  22047  ressmplbas  22077  subrgmpl  22081  mplsubrgcl  22082  opsrtoslem2  22106  mpfrcl  22135  ressply1bas  22287  ressply1evl  22430  evls1addd  22431  evls1muld  22432  evls1vsca  22433  evls1fvcl  22435  evls1maprhm  22436  scmatlss  22582  cpmatsubgpmat  22777  toponsspwpw  22979  basdif0  23010  ntrss2  23114  ordtbas2  23248  ordtbas  23249  cncls  23331  cmpfi  23465  comppfsc  23589  kgentopon  23595  ptpjpre1  23628  xkoccn  23676  prdstopn  23685  uzfbas  23955  utoptop  24291  utopbas  24292  setsmstopn  24535  restmetu  24627  tngtopn  24707  iccntr  24879  metdstri  24909  pi1xfrcnvlem  25115  cphsubrglem  25236  tcphcph  25296  rrxnm  25450  rrxbasefi  25469  ovolshftlem1  25568  ovolshft  25570  ovolscalem1  25572  ovolscalem2  25573  ovolsca  25574  uniioombllem2  25642  uniioombllem3a  25643  uniioombllem3  25644  uniioombllem4  25645  uniioombllem6  25647  itgioo  25875  limcnlp  25937  dvbsss  25961  dvcnvrelem1  26076  dvfsumle  26080  dvfsumabs  26082  pserdv  26489  rlimcnp2  27028  fsumharmonic  27073  chpval2  27279  bday0b  27903  madef  27926  madess  27956  oldssmade  27957  oldss  27960  n0bday  28442  bdayn0p1  28459  bdaypw2n0bndlem  28553  bdaypw2n0bnd  28554  tglnssp  28718  perpln1  28880  perpln2  28881  uhgrspansubgr  29489  clwwlknclwwlkdifnum  30179  ocsh  31483  shsss  31513  speccl  32099  elnlfn  32128  pj3i  32408  sumdmdlem2  32619  fcoinver  32801  ffsrn  32927  ssnnssfz  32986  pfxrn2  33115  ccatws1f1o  33126  cycpmrn  33320  cycpmconjslem2  33332  fxpss  33343  inftmrel  33357  ressply1mon1p  33761  ressply1invg  33762  evls1subd  33765  esplyind  33869  algextdeglem7  34017  algextdeglem8  34018  smatrcl  34090  metidss  34185  fsumcvg4  34244  dya2iocuni  34577  carsgcl  34598  breprexplema  34921  bnj1143  35082  bnj1262  35102  bnj517  35177  kur14lem1  35553  cvmliftmolem2  35629  cvmliftlem15  35645  mrsubrn  35860  msubrn  35876  dfttc2g  36863  poimirlem30  38146  mblfinlem2  38154  sdclem2  38238  sstotbnd2  38270  isbnd3  38280  lkrlss  39716  pmapssat  40380  diass  41663  diaintclN  41679  dia2dimlem13  41697  dibintclN  41788  lcfrlem25  42188  lcdvbasess  42215  mapdin  42283  diophin  43350  rmxyelqirr  43484  itgocn  43738  oaabsb  43868  oege1  43880  oege2  43881  oacl2g  43904  tfsconcatb0  43918  ofoafg  43928  ofoaf  43929  fpwfvss  43985  relexp0a  44289  frege131d  44337  fsovrfovd  44582  clsk1indlem2  44615  clsk1indlem3  44616  mnuprd  44849  unirestss  45699  founiiun0  45765  fsumsupp0  46151  limsupequzlem  46293  dvnprodlem1  46517  ibliooicc  46542  stoweidlem34  46605  stoweidlem59  46630  etransclem24  46829  caratheodory  47099  ovnhoilem1  47172  hspdifhsp  47187  sssmf  47309  smfaddlem2  47335  smflimlem1  47342  smflimlem2  47343  smfmullem4  47365  smfsuplem1  47382  fcoreslem4  47657  fcoresf1  47660  fcoresfo  47662  dfnbgrss  48471  dfnbgrss2  48478  isubgrsubgr  48488  rngchomrnghmresALTV  48898  rngcrescrhmALTV  48899  rhmsubcALTVlem1  48900  funcringcsetcALTV2lem9  48917  ssnn0ssfz  48968  isclatd  49601  nelsubclem  49685  setrec2fun  50310  setrec2mpt  50315