Theorem eqsstrdi 3989

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 3979	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  eqsstrrdi  3990  eqimssd  4001  dmxpss  6170  dmsnopss  6216  iotassuni  6512  fvmptss  7003  fvmptss2  7017  funressn  7157  riotassuni  7408  ordsuci  7806  frxp  8121  suppssdm  8172  suppun  8179  suppss  8189  suppssov1  8192  suppssov2  8193  suppss2  8195  suppssfv  8197  oawordeulem  8538  omwordri  8556  oewordri  8577  mapssfset  8847  fodomr  9115  fodomfir  9286  fipwuni  9385  fipwss  9388  ordtypelem6  9484  inf3lemd  9595  cantnfle  9639  cantnflem2  9658  ttrclselem1  9693  en2other2  9992  ackbij1lem15  10215  ackbij2lem3  10222  cfub  10231  cflecard  10235  cfle  10236  fin23lem13  10315  fin23lem29  10324  compsscnvlem  10353  itunitc1  10403  fpwwe2lem11  10625  grur1a  10803  uzssz  12882  fsuppmapnn0fiublem  14025  fsuppmapnn0fiub  14026  swrdlend  14690  repswswrd  14820  cshimadifsn  14865  xptrrel  15016  relexpnndm  15077  relexpdmd  15080  relexprnd  15084  relexpfldd  15086  rtrclreclem4  15097  limsupgle  15527  isercolllem2  15716  isercolllem3  15717  isercoll  15718  fsumss  15775  sadcaddlem  16514  sadadd2lem  16516  sadadd3  16518  sadcl  16519  sadaddlem  16523  sadasslem  16527  sadeq  16529  smupvallem  16540  smucl  16541  prmreclem4  16978  prmreclem5  16979  1arith  16986  vdwmc2  17038  vdwlem13  17052  ramz2  17083  strfvss  17246  ressbasssg  17296  ressbasssOLD  17299  prdsless  17515  sectss  17808  invss  17817  fullfunc  17964  fthfunc  17965  catccatid  18162  resscatc  18165  catcisolem  18166  catciso  18167  yoniso  18340  gsumpropd2lem  18736  cntzrcl  19396  cntzssv  19397  gsumzmhm  20006  ablfaclem3  20158  rnghmresfn  20703  dfrngc2  20712  rnghmsscmap2  20713  rnghmsscmap  20714  funcrngcsetc  20724  rhmresfn  20732  dfringc2  20741  rhmsscmap2  20742  rhmsscmap  20743  rhmsscrnghm  20749  funcringcsetc  20758  rngcrescrhm  20768  rhmsubclem1  20769  rhmsubclem4  20772  lmhmlsp  21147  evpmss  21704  cssss  21803  frlmplusgval  21882  frlmvscafval  21884  uvcresum  21911  resspsrbas  22091  resspsrvsca  22094  subrgpsr  22095  mplsubglem  22116  ressmplbas  22146  subrgmpl  22150  mplsubrgcl  22151  opsrtoslem2  22175  mpfrcl  22204  ressply1bas  22356  ressply1evl  22498  evls1addd  22499  evls1muld  22500  evls1vsca  22501  evls1fvcl  22503  evls1maprhm  22504  scmatlss  22650  cpmatsubgpmat  22845  toponsspwpw  23047  basdif0  23078  ntrss2  23182  ordtbas2  23316  ordtbas  23317  cncls  23399  cmpfi  23533  comppfsc  23657  kgentopon  23663  ptpjpre1  23696  xkoccn  23744  prdstopn  23753  uzfbas  24023  utoptop  24359  utopbas  24360  setsmstopn  24603  restmetu  24695  tngtopn  24775  iccntr  24947  metdstri  24977  pi1xfrcnvlem  25183  cphsubrglem  25304  tcphcph  25364  rrxnm  25518  rrxbasefi  25537  ovolshftlem1  25636  ovolshft  25638  ovolscalem1  25640  ovolscalem2  25641  ovolsca  25642  uniioombllem2  25710  uniioombllem3a  25711  uniioombllem3  25712  uniioombllem4  25713  uniioombllem6  25715  itgioo  25943  limcnlp  26005  dvbsss  26029  dvcnvrelem1  26144  dvfsumle  26148  dvfsumabs  26150  pserdv  26557  rlimcnp2  27096  fsumharmonic  27141  chpval2  27347  bday0b  27971  madef  27994  madess  28024  oldssmade  28025  oldss  28028  n0bday  28510  bdayn0p1  28527  bdaypw2n0bndlem  28621  bdaypw2n0bnd  28622  tglnssp  28786  perpln1  28948  perpln2  28949  uhgrspansubgr  29581  clwwlknclwwlkdifnum  30271  ocsh  31575  shsss  31605  speccl  32191  elnlfn  32220  pj3i  32500  sumdmdlem2  32711  fcoinver  32889  ffsrn  33013  ssnnssfz  33072  pfxrn2  33200  ccatws1f1o  33211  cycpmrn  33403  cycpmconjslem2  33415  fxpss  33426  inftmrel  33440  ressply1mon1p  33802  ressply1invg  33803  evls1subd  33806  esplyind  33909  algextdeglem7  34057  algextdeglem8  34058  smatrcl  34130  metidss  34225  fsumcvg4  34284  dya2iocuni  34617  carsgcl  34638  breprexplema  34961  bnj1143  35122  bnj1262  35142  bnj517  35217  kur14lem1  35596  cvmliftmolem2  35672  cvmliftlem15  35688  mrsubrn  35903  msubrn  35919  dfttc2g  36905  poimirlem30  38188  mblfinlem2  38196  sdclem2  38280  sstotbnd2  38312  isbnd3  38322  lkrlss  39758  pmapssat  40422  diass  41705  diaintclN  41721  dia2dimlem13  41739  dibintclN  41830  lcfrlem25  42230  lcdvbasess  42257  mapdin  42325  diophin  43394  rmxyelqirr  43528  itgocn  43782  oaabsb  43912  oege1  43924  oege2  43925  oacl2g  43948  tfsconcatb0  43962  ofoafg  43972  ofoaf  43973  fpwfvss  44029  relexp0a  44333  frege131d  44381  fsovrfovd  44626  clsk1indlem2  44659  clsk1indlem3  44660  mnuprd  44877  unirestss  45733  founiiun0  45799  fsumsupp0  46185  limsupequzlem  46327  dvnprodlem1  46551  ibliooicc  46576  stoweidlem34  46639  stoweidlem59  46664  etransclem24  46863  caratheodory  47133  ovnhoilem1  47206  hspdifhsp  47221  sssmf  47343  smfaddlem2  47369  smflimlem1  47376  smflimlem2  47377  smfmullem4  47399  smfsuplem1  47416  fcoreslem4  47691  fcoresf1  47694  fcoresfo  47696  dfnbgrss  48505  dfnbgrss2  48512  isubgrsubgr  48522  rngchomrnghmresALTV  48932  rngcrescrhmALTV  48933  rhmsubcALTVlem1  48934  funcringcsetcALTV2lem9  48951  ssnn0ssfz  49013  isclatd  49645  nelsubclem  49729  setrec2fun  50354  setrec2mpt  50359