Theorem eqsstrdi 3957

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  eqsstrrdi  3958  eqimssd  3969  dmxpss  6181  dmsnopss  6234  iotassuni  6540  fvmptss  7037  fvmptss2  7051  funressn  7195  riotassuni  7448  ordsuci  7856  frxp  8175  suppssdm  8232  suppun  8239  suppss  8249  suppssov1  8252  suppssov2  8253  suppss2  8255  suppssfv  8257  oawordeulem  8600  omwordri  8618  oewordri  8639  mapssfset  8911  fodomr  9185  fodomfir  9357  fipwuni  9455  fipwss  9458  ordtypelem6  9554  inf3lemd  9665  cantnfle  9709  cantnflem2  9728  ttrclselem1  9763  setrec2fun  10010  en2other2  10127  ackbij1lem15  10350  ackbij2lem3  10357  cfub  10365  cflecard  10369  cfle  10370  fin23lem13  10449  fin23lem29  10458  compsscnvlem  10487  itunitc1  10537  fpwwe2lem11  10765  grur1a  10943  uzssz  13026  fsuppmapnn0fiublem  14173  fsuppmapnn0fiub  14174  swrdlend  14845  repswswrd  14977  cshimadifsn  15022  xptrrel  15176  relexpnndm  15237  relexpdmd  15240  relexprnd  15244  relexpfldd  15246  rtrclreclem4  15257  limsupgle  15688  isercolllem2  15877  isercolllem3  15878  isercoll  15879  fsumss  15935  sadcaddlem  16671  sadadd2lem  16673  sadadd3  16675  sadcl  16676  sadaddlem  16680  sadasslem  16684  sadeq  16686  smupvallem  16697  smucl  16698  prmreclem4  17141  prmreclem5  17142  1arith  17149  vdwmc2  17201  vdwlem13  17215  ramz2  17246  strfvss  17409  ressbasssg  17459  ressbasssOLD  17462  prdsless  17684  sectss  17977  invss  17986  fullfunc  18133  fthfunc  18134  catccatid  18331  resscatc  18334  catcisolem  18335  catciso  18336  yoniso  18509  gsumpropd2lem  18918  cntzrcl  19592  cntzssv  19593  gsumzmhm  20202  ablfaclem3  20354  rnghmresfn  20922  dfrngc2  20931  rnghmsscmap2  20932  rnghmsscmap  20933  funcrngcsetc  20943  rhmresfn  20951  dfringc2  20960  rhmsscmap2  20961  rhmsscmap  20962  rhmsscrnghm  20968  funcringcsetc  20977  rngcrescrhm  20987  rhmsubclem1  20988  rhmsubclem4  20991  lmhmlsp  21375  evpmss  21947  cssss  22046  frlmplusgval  22125  frlmvscafval  22127  uvcresum  22154  resspsrbas  22336  resspsrvsca  22339  subrgpsr  22340  mplsubglem  22361  ressmplbas  22391  subrgmpl  22395  mplsubrgcl  22396  opsrtoslem2  22420  mpfrcl  22449  ressply1bas  22601  ressply1evl  22743  evls1addd  22744  evls1muld  22745  evls1vsca  22746  evls1fvcl  22748  evls1maprhm  22749  scmatlss  22895  cpmatsubgpmat  23093  toponsspwpw  23295  basdif0  23326  ntrss2  23430  ordtbas2  23564  ordtbas  23565  cncls  23647  cmpfi  23781  comppfsc  23906  kgentopon  23912  ptpjpre1  23945  xkoccn  23993  prdstopn  24002  uzfbas  24272  utoptop  24608  utopbas  24609  setsmstopn  24852  restmetu  24944  tngtopn  25024  iccntr  25196  metdstri  25226  pi1xfrcnvlem  25432  cphsubrglem  25553  tcphcph  25613  rrxnm  25767  rrxbasefi  25786  ovolshftlem1  25885  ovolshft  25887  ovolscalem1  25889  ovolscalem2  25890  ovolsca  25891  uniioombllem2  25959  uniioombllem3a  25960  uniioombllem3  25961  uniioombllem4  25962  uniioombllem6  25964  itgioo  26191  limcnlp  26253  dvbsss  26277  dvcnvrelem1  26392  dvfsumle  26396  dvfsumabs  26398  pserdv  26813  rlimcnp2  27351  fsumharmonic  27396  chpval2  27602  bday0b  28256  madef  28279  madess  28309  oldssmade  28310  oldss  28313  n0bday  28795  bdayn0p1  28812  bdaypw2n0bndlem  28906  bdaypw2n0bnd  28907  tglnssp  29072  perpln1  29242  perpln2  29243  cgrabasimass  29435  uhgrspansubgr  29929  clwwlknclwwlkdifnum  30628  ocsh  31942  shsss  31972  speccl  32558  elnlfn  32587  pj3i  32867  sumdmdlem2  33078  fcoinver  33296  ffsrn  33416  ssnnssfz  33475  pfxrn2  33603  ccatws1f1o  33610  cycpmrn  33803  cycpmconjslem2  33815  fxpss  33826  inftmrel  33840  ressply1mon1p  34203  ressply1invg  34204  evls1subd  34207  esplyind  34318  algextdeglem7  34466  algextdeglem8  34467  smatrcl  34539  metidss  34634  fsumcvg4  34693  dya2iocuni  35026  carsgcl  35047  breprexplema  35370  bnj1143  35531  bnj1262  35551  bnj517  35626  kur14lem1  36179  cvmliftmolem2  36255  cvmliftlem15  36271  mrsubrn  36486  msubrn  36502  dfttc2g  37509  nvo  38228  nvo3  38230  poimirlem30  38836  mblfinlem2  38844  sdclem2  38942  sstotbnd2  38974  isbnd3  38984  lkrlss  40418  pmapssat  41082  diass  42365  diaintclN  42381  dia2dimlem13  42399  dibintclN  42490  lcfrlem25  42890  lcdvbasess  42917  mapdin  42985  diophin  44049  rmxyelqirr  44183  itgocn  44431  oaabsb  44557  oege1  44569  oege2  44570  oacl2g  44593  tfsconcatb0  44607  ofoafg  44617  ofoaf  44618  fpwfvss  44674  relexp0a  44977  frege131d  45025  fsovrfovd  45270  clsk1indlem2  45303  clsk1indlem3  45304  mnuprd  45521  unirestss  46412  founiiun0  46478  fsumsupp0  46863  limsupequzlem  47005  dvnprodlem1  47229  ibliooicc  47254  stoweidlem34  47317  stoweidlem59  47342  etransclem24  47541  caratheodory  47811  ovnhoilem1  47884  hspdifhsp  47899  sssmf  48021  smfaddlem2  48047  smflimlem1  48054  smflimlem2  48055  smfmullem4  48077  smfsuplem1  48094  fcoreslem4  48409  fcoresf1  48412  fcoresfo  48414  dfnbgrss  49223  dfnbgrss2  49230  isubgrsubgr  49240  rngchomrnghmresALTV  49649  rngcrescrhmALTV  49650  rhmsubcALTVlem1  49651  funcringcsetcALTV2lem9  49668  ssnn0ssfz  49792  isclatd  50428  nelsubclem  50512  setrec2mpt  51196