Theorem eqsstrdi 3971

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  eqsstrrdi  3972  dmxpss  6063  dmsnopss  6106  iotassuni  6397  fvmptss  6869  fvmptss2  6882  fimacnvOLD  6930  funressn  7013  riotassuni  7253  frxp  7938  suppssdm  7964  suppun  7971  suppss  7981  suppssOLD  7982  suppssov1  7985  suppss2  7987  suppssfv  7989  wfrlem15OLD  8125  oawordeulem  8347  omwordri  8365  oewordri  8385  mapssfset  8597  fodomr  8864  fipwuni  9115  fipwss  9118  ordtypelem6  9212  inf3lemd  9315  cantnfle  9359  cantnflem2  9378  trpredlem1  9405  en2other2  9696  ackbij1lem15  9921  ackbij2lem3  9928  cfub  9936  cflecard  9940  cfle  9941  fin23lem13  10019  fin23lem29  10028  compsscnvlem  10057  itunitc1  10107  fpwwe2lem11  10328  grur1a  10506  uzssz  12532  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  swrdlend  14294  repswswrd  14425  cshimadifsn  14470  xptrrel  14619  relexpnndm  14680  relexpdmd  14683  relexprnd  14687  relexpfldd  14689  rtrclreclem4  14700  limsupgle  15114  isercolllem2  15305  isercolllem3  15306  isercoll  15307  fsumss  15365  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadcl  16097  sadaddlem  16101  sadasslem  16105  sadeq  16107  smupvallem  16118  smucl  16119  prmreclem4  16548  prmreclem5  16549  1arith  16556  vdwmc2  16608  vdwlem13  16622  ramz2  16653  strfvss  16816  ressbasss  16876  prdsless  17091  sectss  17381  invss  17390  fullfunc  17538  fthfunc  17539  catccatid  17737  resscatc  17740  catcisolem  17741  catciso  17742  yoniso  17919  gsumpropd2lem  18278  cntzrcl  18848  cntzssv  18849  gsumzmhm  19453  ablfaclem3  19605  lmhmlsp  20226  evpmss  20703  cssss  20802  frlmplusgval  20881  frlmvscafval  20883  uvcresum  20910  resspsrbas  21094  resspsrvsca  21097  subrgpsr  21098  mplsubglem  21115  ressmplbas  21139  subrgmpl  21143  mpfrcl  21205  ressply1bas  21310  scmatlss  21582  cpmatsubgpmat  21777  toponsspwpw  21979  basdif0  22011  ntrss2  22116  ordtbas2  22250  ordtbas  22251  cncls  22333  cmpfi  22467  comppfsc  22591  kgentopon  22597  ptpjpre1  22630  xkoccn  22678  prdstopn  22687  uzfbas  22957  utoptop  23294  utopbas  23295  setsmstopn  23539  restmetu  23632  tngtopn  23720  iccntr  23890  metdstri  23920  pi1xfrcnvlem  24125  cphsubrglem  24246  tcphcph  24306  rrxnm  24460  rrxbasefi  24479  ovolshftlem1  24578  ovolshft  24580  ovolscalem1  24582  ovolscalem2  24583  ovolsca  24584  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem6  24657  itgioo  24885  limcnlp  24947  dvbsss  24971  dvcnvrelem1  25086  dvfsumle  25090  dvfsumabs  25092  pserdv  25493  rlimcnp2  26021  fsumharmonic  26066  chpval2  26271  tglnssp  26817  perpln1  26975  perpln2  26976  uhgrspansubgr  27561  clwwlknclwwlkdifnum  28245  ocsh  29546  shsss  29576  speccl  30162  elnlfn  30191  pj3i  30471  sumdmdlem2  30682  fcoinver  30847  ffsrn  30966  ssnnssfz  31010  pfxrn2  31116  cycpmrn  31312  cycpmconjslem2  31324  inftmrel  31336  smatrcl  31648  metidss  31743  fsumcvg4  31802  dya2iocuni  32150  carsgcl  32171  breprexplema  32510  bnj1143  32670  bnj1262  32690  bnj517  32765  kur14lem1  33068  cvmliftmolem2  33144  cvmliftlem15  33160  mrsubrn  33375  msubrn  33391  ttrclselem1  33711  bday0b  33951  madef  33967  madess  33986  oldssmade  33987  poimirlem30  35734  mblfinlem2  35742  sdclem2  35827  sstotbnd2  35859  isbnd3  35869  lkrlss  37036  pmapssat  37700  diass  38983  diaintclN  38999  dia2dimlem13  39017  dibintclN  39108  lcfrlem25  39508  lcdvbasess  39535  mapdin  39603  eqimssd  40111  sn-iotassuni  40122  diophin  40510  itgocn  40905  relexp0a  41213  frege131d  41261  fsovrfovd  41506  clsk1indlem2  41541  clsk1indlem3  41542  mnuprd  41783  unirestss  42562  founiiun0  42617  fsumsupp0  43009  limsupequzlem  43153  ibliooicc  43402  stoweidlem34  43465  stoweidlem59  43490  etransclem24  43689  caratheodory  43956  ovnhoilem1  44029  hspdifhsp  44044  smfaddlem2  44186  smflimlem1  44193  smflimlem2  44194  smfmullem4  44215  smfsuplem1  44231  fcoreslem4  44447  fcoresf1  44450  fcoresfo  44452  rnghmresfn  45409  dfrngc2  45418  rnghmsscmap2  45419  rnghmsscmap  45420  rngchomrnghmresALTV  45442  funcrngcsetc  45444  rhmresfn  45455  dfringc2  45464  rhmsscmap2  45465  rhmsscmap  45466  rhmsscrnghm  45472  funcringcsetc  45481  funcringcsetcALTV2lem9  45490  rngcrescrhm  45531  rhmsubclem1  45532  rhmsubclem4  45535  rngcrescrhmALTV  45549  rhmsubcALTVlem1  45550  ssnn0ssfz  45573  isclatd  46157  setrec2fun  46284