Theorem eqsstrdi 3976

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916

This theorem is referenced by:  eqsstrrdi  3977  eqimssd  3988  dmxpss  6127  dmsnopss  6170  iotassuni  6465  fvmptss  6951  fvmptss2  6965  funressn  7102  riotassuni  7353  ordsuci  7751  frxp  8066  suppssdm  8117  suppun  8124  suppss  8134  suppssov1  8137  suppssov2  8138  suppss2  8140  suppssfv  8142  oawordeulem  8479  omwordri  8497  oewordri  8518  mapssfset  8786  fodomr  9054  fodomfir  9226  fipwuni  9327  fipwss  9330  ordtypelem6  9426  inf3lemd  9534  cantnfle  9578  cantnflem2  9597  ttrclselem1  9632  en2other2  9917  ackbij1lem15  10141  ackbij2lem3  10148  cfub  10157  cflecard  10161  cfle  10162  fin23lem13  10240  fin23lem29  10249  compsscnvlem  10278  itunitc1  10328  fpwwe2lem11  10550  grur1a  10728  uzssz  12770  fsuppmapnn0fiublem  13911  fsuppmapnn0fiub  13912  swrdlend  14575  repswswrd  14705  cshimadifsn  14750  xptrrel  14901  relexpnndm  14962  relexpdmd  14965  relexprnd  14969  relexpfldd  14971  rtrclreclem4  14982  limsupgle  15398  isercolllem2  15587  isercolllem3  15588  isercoll  15589  fsumss  15646  sadcaddlem  16382  sadadd2lem  16384  sadadd3  16386  sadcl  16387  sadaddlem  16391  sadasslem  16395  sadeq  16397  smupvallem  16408  smucl  16409  prmreclem4  16845  prmreclem5  16846  1arith  16853  vdwmc2  16905  vdwlem13  16919  ramz2  16950  strfvss  17112  ressbasssg  17162  ressbasssOLD  17165  prdsless  17381  sectss  17674  invss  17683  fullfunc  17830  fthfunc  17831  catccatid  18028  resscatc  18031  catcisolem  18032  catciso  18033  yoniso  18206  gsumpropd2lem  18602  cntzrcl  19254  cntzssv  19255  gsumzmhm  19864  ablfaclem3  20016  rnghmresfn  20550  dfrngc2  20559  rnghmsscmap2  20560  rnghmsscmap  20561  funcrngcsetc  20571  rhmresfn  20579  dfringc2  20588  rhmsscmap2  20589  rhmsscmap  20590  rhmsscrnghm  20596  funcringcsetc  20605  rngcrescrhm  20615  rhmsubclem1  20616  rhmsubclem4  20619  lmhmlsp  20999  evpmss  21539  cssss  21638  frlmplusgval  21717  frlmvscafval  21719  uvcresum  21746  resspsrbas  21927  resspsrvsca  21930  subrgpsr  21931  mplsubglem  21952  ressmplbas  21981  subrgmpl  21985  opsrtoslem2  22009  mpfrcl  22038  ressply1bas  22167  ressply1evl  22312  evls1addd  22313  evls1muld  22314  evls1vsca  22315  evls1fvcl  22317  evls1maprhm  22318  scmatlss  22467  cpmatsubgpmat  22662  toponsspwpw  22864  basdif0  22895  ntrss2  22999  ordtbas2  23133  ordtbas  23134  cncls  23216  cmpfi  23350  comppfsc  23474  kgentopon  23480  ptpjpre1  23513  xkoccn  23561  prdstopn  23570  uzfbas  23840  utoptop  24176  utopbas  24177  setsmstopn  24420  restmetu  24512  tngtopn  24592  iccntr  24764  metdstri  24794  pi1xfrcnvlem  25010  cphsubrglem  25131  tcphcph  25191  rrxnm  25345  rrxbasefi  25364  ovolshftlem1  25464  ovolshft  25466  ovolscalem1  25468  ovolscalem2  25469  ovolsca  25470  uniioombllem2  25538  uniioombllem3a  25539  uniioombllem3  25540  uniioombllem4  25541  uniioombllem6  25543  itgioo  25771  limcnlp  25833  dvbsss  25857  dvcnvrelem1  25976  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  pserdv  26393  rlimcnp2  26930  fsumharmonic  26976  chpval2  27183  bday0b  27801  madef  27824  madess  27848  oldssmade  27849  oldss  27850  n0sbday  28312  bdayn0p1  28327  bdaypw2n0s  28420  tglnssp  28573  perpln1  28731  perpln2  28732  uhgrspansubgr  29313  clwwlknclwwlkdifnum  30004  ocsh  31307  shsss  31337  speccl  31923  elnlfn  31952  pj3i  32232  sumdmdlem2  32443  fcoinver  32628  ffsrn  32756  ssnnssfz  32816  pfxrn2  32971  ccatws1f1o  32982  cycpmrn  33174  cycpmconjslem2  33186  fxpss  33197  inftmrel  33211  ressply1mon1p  33598  ressply1invg  33599  evls1subd  33602  esplyind  33680  algextdeglem7  33829  algextdeglem8  33830  smatrcl  33902  metidss  33997  fsumcvg4  34056  dya2iocuni  34389  carsgcl  34410  breprexplema  34736  bnj1143  34895  bnj1262  34915  bnj517  34990  kur14lem1  35349  cvmliftmolem2  35425  cvmliftlem15  35441  mrsubrn  35656  msubrn  35672  poimirlem30  37790  mblfinlem2  37798  sdclem2  37882  sstotbnd2  37914  isbnd3  37924  lkrlss  39294  pmapssat  39958  diass  41241  diaintclN  41257  dia2dimlem13  41275  dibintclN  41366  lcfrlem25  41766  lcdvbasess  41793  mapdin  41861  mplsubrgcl  42743  diophin  42956  rmxyelqirr  43094  itgocn  43348  oaabsb  43478  oege1  43490  oege2  43491  oacl2g  43514  tfsconcatb0  43528  ofoafg  43538  ofoaf  43539  fpwfvss  43595  relexp0a  43899  frege131d  43947  fsovrfovd  44192  clsk1indlem2  44225  clsk1indlem3  44226  mnuprd  44459  unirestss  45310  founiiun0  45376  fsumsupp0  45766  limsupequzlem  45908  dvnprodlem1  46132  ibliooicc  46157  stoweidlem34  46220  stoweidlem59  46245  etransclem24  46444  caratheodory  46714  ovnhoilem1  46787  hspdifhsp  46802  smfaddlem2  46950  smflimlem1  46957  smflimlem2  46958  smfmullem4  46980  smfsuplem1  46997  fcoreslem4  47254  fcoresf1  47257  fcoresfo  47259  dfnbgrss  48040  dfnbgrss2  48047  isubgrsubgr  48057  rngchomrnghmresALTV  48467  rngcrescrhmALTV  48468  rhmsubcALTVlem1  48469  funcringcsetcALTV2lem9  48486  ssnn0ssfz  48537  isclatd  49170  nelsubclem  49254  setrec2fun  49879  setrec2mpt  49884