Theorem eqsstrdi 3975

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  eqsstrrdi  3976  eqimssd  3987  dmxpss  6163  dmsnopss  6214  iotassuni  6512  fvmptss  7004  fvmptss2  7018  funressn  7161  riotassuni  7415  ordsuci  7820  frxp  8136  suppssdm  8187  suppun  8194  suppss  8204  suppssov1  8207  suppssov2  8208  suppss2  8210  suppssfv  8212  oawordeulem  8555  omwordri  8573  oewordri  8594  mapssfset  8866  fodomr  9140  fodomfir  9312  fipwuni  9411  fipwss  9414  ordtypelem6  9510  inf3lemd  9621  cantnfle  9665  cantnflem2  9684  ttrclselem1  9719  setrec2fun  9966  en2other2  10081  ackbij1lem15  10304  ackbij2lem3  10311  cfub  10319  cflecard  10323  cfle  10324  fin23lem13  10403  fin23lem29  10412  compsscnvlem  10441  itunitc1  10491  fpwwe2lem11  10719  grur1a  10897  uzssz  12979  fsuppmapnn0fiublem  14126  fsuppmapnn0fiub  14127  swrdlend  14796  repswswrd  14928  cshimadifsn  14973  xptrrel  15126  relexpnndm  15187  relexpdmd  15190  relexprnd  15194  relexpfldd  15196  rtrclreclem4  15207  limsupgle  15637  isercolllem2  15826  isercolllem3  15827  isercoll  15828  fsumss  15884  sadcaddlem  16620  sadadd2lem  16622  sadadd3  16624  sadcl  16625  sadaddlem  16629  sadasslem  16633  sadeq  16635  smupvallem  16646  smucl  16647  prmreclem4  17090  prmreclem5  17091  1arith  17098  vdwmc2  17150  vdwlem13  17164  ramz2  17195  strfvss  17358  ressbasssg  17408  ressbasssOLD  17411  prdsless  17627  sectss  17920  invss  17929  fullfunc  18076  fthfunc  18077  catccatid  18274  resscatc  18277  catcisolem  18278  catciso  18279  yoniso  18452  gsumpropd2lem  18861  cntzrcl  19534  cntzssv  19535  gsumzmhm  20144  ablfaclem3  20296  rnghmresfn  20864  dfrngc2  20873  rnghmsscmap2  20874  rnghmsscmap  20875  funcrngcsetc  20885  rhmresfn  20893  dfringc2  20902  rhmsscmap2  20903  rhmsscmap  20904  rhmsscrnghm  20910  funcringcsetc  20919  rngcrescrhm  20929  rhmsubclem1  20930  rhmsubclem4  20933  lmhmlsp  21317  evpmss  21885  cssss  21984  frlmplusgval  22063  frlmvscafval  22065  uvcresum  22092  resspsrbas  22274  resspsrvsca  22277  subrgpsr  22278  mplsubglem  22299  ressmplbas  22329  subrgmpl  22333  mplsubrgcl  22334  opsrtoslem2  22358  mpfrcl  22387  ressply1bas  22539  ressply1evl  22681  evls1addd  22682  evls1muld  22683  evls1vsca  22684  evls1fvcl  22686  evls1maprhm  22687  scmatlss  22833  cpmatsubgpmat  23031  toponsspwpw  23233  basdif0  23264  ntrss2  23368  ordtbas2  23502  ordtbas  23503  cncls  23585  cmpfi  23719  comppfsc  23844  kgentopon  23850  ptpjpre1  23883  xkoccn  23931  prdstopn  23940  uzfbas  24210  utoptop  24546  utopbas  24547  setsmstopn  24790  restmetu  24882  tngtopn  24962  iccntr  25134  metdstri  25164  pi1xfrcnvlem  25370  cphsubrglem  25491  tcphcph  25551  rrxnm  25705  rrxbasefi  25724  ovolshftlem1  25823  ovolshft  25825  ovolscalem1  25827  ovolscalem2  25828  ovolsca  25829  uniioombllem2  25897  uniioombllem3a  25898  uniioombllem3  25899  uniioombllem4  25900  uniioombllem6  25902  itgioo  26129  limcnlp  26191  dvbsss  26215  dvcnvrelem1  26330  dvfsumle  26334  dvfsumabs  26336  pserdv  26749  rlimcnp2  27287  fsumharmonic  27332  chpval2  27538  bday0b  28192  madef  28215  madess  28245  oldssmade  28246  oldss  28249  n0bday  28731  bdayn0p1  28748  bdaypw2n0bndlem  28842  bdaypw2n0bnd  28843  tglnssp  29008  perpln1  29178  perpln2  29179  cgrabasimass  29371  uhgrspansubgr  29865  clwwlknclwwlkdifnum  30564  ocsh  31878  shsss  31908  speccl  32494  elnlfn  32523  pj3i  32803  sumdmdlem2  33014  fcoinver  33191  ffsrn  33313  ssnnssfz  33372  pfxrn2  33500  ccatws1f1o  33507  cycpmrn  33697  cycpmconjslem2  33709  fxpss  33720  inftmrel  33734  ressply1mon1p  34093  ressply1invg  34094  evls1subd  34097  esplyind  34200  algextdeglem7  34348  algextdeglem8  34349  smatrcl  34421  metidss  34516  fsumcvg4  34575  dya2iocuni  34908  carsgcl  34929  breprexplema  35252  bnj1143  35413  bnj1262  35433  bnj517  35508  kur14lem1  35950  cvmliftmolem2  36026  cvmliftlem15  36042  mrsubrn  36257  msubrn  36273  dfttc2g  37274  poimirlem30  38548  mblfinlem2  38556  sdclem2  38656  sstotbnd2  38688  isbnd3  38698  lkrlss  40132  pmapssat  40796  diass  42079  diaintclN  42095  dia2dimlem13  42113  dibintclN  42204  lcfrlem25  42604  lcdvbasess  42631  mapdin  42699  diophin  43762  rmxyelqirr  43896  itgocn  44150  oaabsb  44280  oege1  44292  oege2  44293  oacl2g  44316  tfsconcatb0  44330  ofoafg  44340  ofoaf  44341  fpwfvss  44397  relexp0a  44701  frege131d  44749  fsovrfovd  44994  clsk1indlem2  45027  clsk1indlem3  45028  mnuprd  45245  unirestss  46108  founiiun0  46174  fsumsupp0  46559  limsupequzlem  46701  dvnprodlem1  46925  ibliooicc  46950  stoweidlem34  47013  stoweidlem59  47038  etransclem24  47237  caratheodory  47507  ovnhoilem1  47580  hspdifhsp  47595  sssmf  47717  smfaddlem2  47743  smflimlem1  47750  smflimlem2  47751  smfmullem4  47773  smfsuplem1  47790  fcoreslem4  48105  fcoresf1  48108  fcoresfo  48110  dfnbgrss  48919  dfnbgrss2  48926  isubgrsubgr  48936  rngchomrnghmresALTV  49345  rngcrescrhmALTV  49346  rhmsubcALTVlem1  49347  funcringcsetcALTV2lem9  49364  ssnn0ssfz  49430  isclatd  50060  nelsubclem  50144  setrec2mpt  50759