Theorem eqsstrdi 3966

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

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 2708

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

This theorem is referenced by:  eqsstrrdi  3967  eqimssd  3978  dmxpss  6135  dmsnopss  6178  iotassuni  6473  fvmptss  6960  fvmptss2  6974  funressn  7113  riotassuni  7364  ordsuci  7762  frxp  8076  suppssdm  8127  suppun  8134  suppss  8144  suppssov1  8147  suppssov2  8148  suppss2  8150  suppssfv  8152  oawordeulem  8489  omwordri  8507  oewordri  8528  mapssfset  8798  fodomr  9066  fodomfir  9238  fipwuni  9339  fipwss  9342  ordtypelem6  9438  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  12809  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  swrdlend  14616  repswswrd  14746  cshimadifsn  14791  xptrrel  14942  relexpnndm  15003  relexpdmd  15006  relexprnd  15010  relexpfldd  15012  rtrclreclem4  15023  limsupgle  15439  isercolllem2  15628  isercolllem3  15629  isercoll  15630  fsumss  15687  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadcl  16431  sadaddlem  16435  sadasslem  16439  sadeq  16441  smupvallem  16452  smucl  16453  prmreclem4  16890  prmreclem5  16891  1arith  16898  vdwmc2  16950  vdwlem13  16964  ramz2  16995  strfvss  17157  ressbasssg  17207  ressbasssOLD  17210  prdsless  17426  sectss  17719  invss  17728  fullfunc  17875  fthfunc  17876  catccatid  18073  resscatc  18076  catcisolem  18077  catciso  18078  yoniso  18251  gsumpropd2lem  18647  cntzrcl  19302  cntzssv  19303  gsumzmhm  19912  ablfaclem3  20064  rnghmresfn  20596  dfrngc2  20605  rnghmsscmap2  20606  rnghmsscmap  20607  funcrngcsetc  20617  rhmresfn  20625  dfringc2  20634  rhmsscmap2  20635  rhmsscmap  20636  rhmsscrnghm  20642  funcringcsetc  20651  rngcrescrhm  20661  rhmsubclem1  20662  rhmsubclem4  20665  lmhmlsp  21044  evpmss  21566  cssss  21665  frlmplusgval  21744  frlmvscafval  21746  uvcresum  21773  resspsrbas  21952  resspsrvsca  21955  subrgpsr  21956  mplsubglem  21977  ressmplbas  22006  subrgmpl  22010  opsrtoslem2  22034  mpfrcl  22063  ressply1bas  22192  ressply1evl  22335  evls1addd  22336  evls1muld  22337  evls1vsca  22338  evls1fvcl  22340  evls1maprhm  22341  scmatlss  22490  cpmatsubgpmat  22685  toponsspwpw  22887  basdif0  22918  ntrss2  23022  ordtbas2  23156  ordtbas  23157  cncls  23239  cmpfi  23373  comppfsc  23497  kgentopon  23503  ptpjpre1  23536  xkoccn  23584  prdstopn  23593  uzfbas  23863  utoptop  24199  utopbas  24200  setsmstopn  24443  restmetu  24535  tngtopn  24615  iccntr  24787  metdstri  24817  pi1xfrcnvlem  25023  cphsubrglem  25144  tcphcph  25204  rrxnm  25358  rrxbasefi  25377  ovolshftlem1  25476  ovolshft  25478  ovolscalem1  25480  ovolscalem2  25481  ovolsca  25482  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem6  25555  itgioo  25783  limcnlp  25845  dvbsss  25869  dvcnvrelem1  25984  dvfsumle  25988  dvfsumabs  25990  pserdv  26394  rlimcnp2  26930  fsumharmonic  26975  chpval2  27181  bday0b  27805  madef  27828  madess  27858  oldssmade  27859  oldss  27862  n0bday  28344  bdayn0p1  28361  bdaypw2n0bndlem  28455  bdaypw2n0bnd  28456  tglnssp  28620  perpln1  28778  perpln2  28779  uhgrspansubgr  29360  clwwlknclwwlkdifnum  30050  ocsh  31354  shsss  31384  speccl  31970  elnlfn  31999  pj3i  32279  sumdmdlem2  32490  fcoinver  32674  ffsrn  32801  ssnnssfz  32860  pfxrn2  33000  ccatws1f1o  33011  cycpmrn  33204  cycpmconjslem2  33216  fxpss  33227  inftmrel  33241  ressply1mon1p  33628  ressply1invg  33629  evls1subd  33632  esplyind  33719  algextdeglem7  33867  algextdeglem8  33868  smatrcl  33940  metidss  34035  fsumcvg4  34094  dya2iocuni  34427  carsgcl  34448  breprexplema  34774  bnj1143  34932  bnj1262  34952  bnj517  35027  kur14lem1  35388  cvmliftmolem2  35464  cvmliftlem15  35480  mrsubrn  35695  msubrn  35711  dfttc2g  36688  poimirlem30  37971  mblfinlem2  37979  sdclem2  38063  sstotbnd2  38095  isbnd3  38105  lkrlss  39541  pmapssat  40205  diass  41488  diaintclN  41504  dia2dimlem13  41522  dibintclN  41613  lcfrlem25  42013  lcdvbasess  42040  mapdin  42108  mplsubrgcl  42991  diophin  43204  rmxyelqirr  43338  itgocn  43592  oaabsb  43722  oege1  43734  oege2  43735  oacl2g  43758  tfsconcatb0  43772  ofoafg  43782  ofoaf  43783  fpwfvss  43839  relexp0a  44143  frege131d  44191  fsovrfovd  44436  clsk1indlem2  44469  clsk1indlem3  44470  mnuprd  44703  unirestss  45554  founiiun0  45620  fsumsupp0  46008  limsupequzlem  46150  dvnprodlem1  46374  ibliooicc  46399  stoweidlem34  46462  stoweidlem59  46487  etransclem24  46686  caratheodory  46956  ovnhoilem1  47029  hspdifhsp  47044  smfaddlem2  47192  smflimlem1  47199  smflimlem2  47200  smfmullem4  47222  smfsuplem1  47239  fcoreslem4  47514  fcoresf1  47517  fcoresfo  47519  dfnbgrss  48328  dfnbgrss2  48335  isubgrsubgr  48345  rngchomrnghmresALTV  48755  rngcrescrhmALTV  48756  rhmsubcALTVlem1  48757  funcringcsetcALTV2lem9  48774  ssnn0ssfz  48825  isclatd  49458  nelsubclem  49542  setrec2fun  50167  setrec2mpt  50172