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 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  eqsstrrdi  3981  eqimssd  3992  dmxpss  6137  dmsnopss  6180  iotassuni  6475  fvmptss  6962  fvmptss2  6976  funressn  7114  riotassuni  7365  ordsuci  7763  frxp  8078  suppssdm  8129  suppun  8136  suppss  8146  suppssov1  8149  suppssov2  8150  suppss2  8152  suppssfv  8154  oawordeulem  8491  omwordri  8509  oewordri  8530  mapssfset  8800  fodomr  9068  fodomfir  9240  fipwuni  9341  fipwss  9344  ordtypelem6  9440  inf3lemd  9548  cantnfle  9592  cantnflem2  9611  ttrclselem1  9646  en2other2  9931  ackbij1lem15  10155  ackbij2lem3  10162  cfub  10171  cflecard  10175  cfle  10176  fin23lem13  10254  fin23lem29  10263  compsscnvlem  10292  itunitc1  10342  fpwwe2lem11  10564  grur1a  10742  uzssz  12784  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  swrdlend  14589  repswswrd  14719  cshimadifsn  14764  xptrrel  14915  relexpnndm  14976  relexpdmd  14979  relexprnd  14983  relexpfldd  14985  rtrclreclem4  14996  limsupgle  15412  isercolllem2  15601  isercolllem3  15602  isercoll  15603  fsumss  15660  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadcl  16401  sadaddlem  16405  sadasslem  16409  sadeq  16411  smupvallem  16422  smucl  16423  prmreclem4  16859  prmreclem5  16860  1arith  16867  vdwmc2  16919  vdwlem13  16933  ramz2  16964  strfvss  17126  ressbasssg  17176  ressbasssOLD  17179  prdsless  17395  sectss  17688  invss  17697  fullfunc  17844  fthfunc  17845  catccatid  18042  resscatc  18045  catcisolem  18046  catciso  18047  yoniso  18220  gsumpropd2lem  18616  cntzrcl  19268  cntzssv  19269  gsumzmhm  19878  ablfaclem3  20030  rnghmresfn  20564  dfrngc2  20573  rnghmsscmap2  20574  rnghmsscmap  20575  funcrngcsetc  20585  rhmresfn  20593  dfringc2  20602  rhmsscmap2  20603  rhmsscmap  20604  rhmsscrnghm  20610  funcringcsetc  20619  rngcrescrhm  20629  rhmsubclem1  20630  rhmsubclem4  20633  lmhmlsp  21013  evpmss  21553  cssss  21652  frlmplusgval  21731  frlmvscafval  21733  uvcresum  21760  resspsrbas  21941  resspsrvsca  21944  subrgpsr  21945  mplsubglem  21966  ressmplbas  21995  subrgmpl  21999  opsrtoslem2  22023  mpfrcl  22052  ressply1bas  22181  ressply1evl  22326  evls1addd  22327  evls1muld  22328  evls1vsca  22329  evls1fvcl  22331  evls1maprhm  22332  scmatlss  22481  cpmatsubgpmat  22676  toponsspwpw  22878  basdif0  22909  ntrss2  23013  ordtbas2  23147  ordtbas  23148  cncls  23230  cmpfi  23364  comppfsc  23488  kgentopon  23494  ptpjpre1  23527  xkoccn  23575  prdstopn  23584  uzfbas  23854  utoptop  24190  utopbas  24191  setsmstopn  24434  restmetu  24526  tngtopn  24606  iccntr  24778  metdstri  24808  pi1xfrcnvlem  25024  cphsubrglem  25145  tcphcph  25205  rrxnm  25359  rrxbasefi  25378  ovolshftlem1  25478  ovolshft  25480  ovolscalem1  25482  ovolscalem2  25483  ovolsca  25484  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem6  25557  itgioo  25785  limcnlp  25847  dvbsss  25871  dvcnvrelem1  25990  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  pserdv  26407  rlimcnp2  26944  fsumharmonic  26990  chpval2  27197  bday0b  27821  madef  27844  madess  27874  oldssmade  27875  oldss  27878  n0bday  28360  bdayn0p1  28377  bdaypw2n0bndlem  28471  bdaypw2n0bnd  28472  tglnssp  28636  perpln1  28794  perpln2  28795  uhgrspansubgr  29376  clwwlknclwwlkdifnum  30067  ocsh  31371  shsss  31401  speccl  31987  elnlfn  32016  pj3i  32296  sumdmdlem2  32507  fcoinver  32691  ffsrn  32818  ssnnssfz  32878  pfxrn2  33033  ccatws1f1o  33044  cycpmrn  33237  cycpmconjslem2  33249  fxpss  33260  inftmrel  33274  ressply1mon1p  33661  ressply1invg  33662  evls1subd  33665  esplyind  33752  algextdeglem7  33901  algextdeglem8  33902  smatrcl  33974  metidss  34069  fsumcvg4  34128  dya2iocuni  34461  carsgcl  34482  breprexplema  34808  bnj1143  34966  bnj1262  34986  bnj517  35061  kur14lem1  35422  cvmliftmolem2  35498  cvmliftlem15  35514  mrsubrn  35729  msubrn  35745  poimirlem30  37901  mblfinlem2  37909  sdclem2  37993  sstotbnd2  38025  isbnd3  38035  lkrlss  39471  pmapssat  40135  diass  41418  diaintclN  41434  dia2dimlem13  41452  dibintclN  41543  lcfrlem25  41943  lcdvbasess  41970  mapdin  42038  mplsubrgcl  42916  diophin  43129  rmxyelqirr  43267  itgocn  43521  oaabsb  43651  oege1  43663  oege2  43664  oacl2g  43687  tfsconcatb0  43701  ofoafg  43711  ofoaf  43712  fpwfvss  43768  relexp0a  44072  frege131d  44120  fsovrfovd  44365  clsk1indlem2  44398  clsk1indlem3  44399  mnuprd  44632  unirestss  45483  founiiun0  45549  fsumsupp0  45938  limsupequzlem  46080  dvnprodlem1  46304  ibliooicc  46329  stoweidlem34  46392  stoweidlem59  46417  etransclem24  46616  caratheodory  46886  ovnhoilem1  46959  hspdifhsp  46974  smfaddlem2  47122  smflimlem1  47129  smflimlem2  47130  smfmullem4  47152  smfsuplem1  47169  fcoreslem4  47426  fcoresf1  47429  fcoresfo  47431  dfnbgrss  48212  dfnbgrss2  48219  isubgrsubgr  48229  rngchomrnghmresALTV  48639  rngcrescrhmALTV  48640  rhmsubcALTVlem1  48641  funcringcsetcALTV2lem9  48658  ssnn0ssfz  48709  isclatd  49342  nelsubclem  49426  setrec2fun  50051  setrec2mpt  50056