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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqsstrrdi  3981  eqimssd  3992  dmxpss  6120  dmsnopss  6163  iotassuni  6457  fvmptss  6942  fvmptss2  6956  funressn  7093  riotassuni  7346  ordsuci  7744  frxp  8059  suppssdm  8110  suppun  8117  suppss  8127  suppssov1  8130  suppssov2  8131  suppss2  8133  suppssfv  8135  oawordeulem  8472  omwordri  8490  oewordri  8510  mapssfset  8778  fodomr  9045  fodomfir  9218  fipwuni  9316  fipwss  9319  ordtypelem6  9415  inf3lemd  9523  cantnfle  9567  cantnflem2  9586  ttrclselem1  9621  en2other2  9903  ackbij1lem15  10127  ackbij2lem3  10134  cfub  10143  cflecard  10147  cfle  10148  fin23lem13  10226  fin23lem29  10235  compsscnvlem  10264  itunitc1  10314  fpwwe2lem11  10535  grur1a  10713  uzssz  12756  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  swrdlend  14560  repswswrd  14690  cshimadifsn  14736  xptrrel  14887  relexpnndm  14948  relexpdmd  14951  relexprnd  14955  relexpfldd  14957  rtrclreclem4  14968  limsupgle  15384  isercolllem2  15573  isercolllem3  15574  isercoll  15575  fsumss  15632  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadcl  16373  sadaddlem  16377  sadasslem  16381  sadeq  16383  smupvallem  16394  smucl  16395  prmreclem4  16831  prmreclem5  16832  1arith  16839  vdwmc2  16891  vdwlem13  16905  ramz2  16936  strfvss  17098  ressbasssg  17148  ressbasssOLD  17151  prdsless  17367  sectss  17659  invss  17668  fullfunc  17815  fthfunc  17816  catccatid  18013  resscatc  18016  catcisolem  18017  catciso  18018  yoniso  18191  gsumpropd2lem  18553  cntzrcl  19206  cntzssv  19207  gsumzmhm  19816  ablfaclem3  19968  rnghmresfn  20504  dfrngc2  20513  rnghmsscmap2  20514  rnghmsscmap  20515  funcrngcsetc  20525  rhmresfn  20533  dfringc2  20542  rhmsscmap2  20543  rhmsscmap  20544  rhmsscrnghm  20550  funcringcsetc  20559  rngcrescrhm  20569  rhmsubclem1  20570  rhmsubclem4  20573  lmhmlsp  20953  evpmss  21493  cssss  21592  frlmplusgval  21671  frlmvscafval  21673  uvcresum  21700  resspsrbas  21881  resspsrvsca  21884  subrgpsr  21885  mplsubglem  21906  ressmplbas  21933  subrgmpl  21937  opsrtoslem2  21961  mpfrcl  21990  ressply1bas  22111  ressply1evl  22255  evls1addd  22256  evls1muld  22257  evls1vsca  22258  evls1fvcl  22260  evls1maprhm  22261  scmatlss  22410  cpmatsubgpmat  22605  toponsspwpw  22807  basdif0  22838  ntrss2  22942  ordtbas2  23076  ordtbas  23077  cncls  23159  cmpfi  23293  comppfsc  23417  kgentopon  23423  ptpjpre1  23456  xkoccn  23504  prdstopn  23513  uzfbas  23783  utoptop  24120  utopbas  24121  setsmstopn  24364  restmetu  24456  tngtopn  24536  iccntr  24708  metdstri  24738  pi1xfrcnvlem  24954  cphsubrglem  25075  tcphcph  25135  rrxnm  25289  rrxbasefi  25308  ovolshftlem1  25408  ovolshft  25410  ovolscalem1  25412  ovolscalem2  25413  ovolsca  25414  uniioombllem2  25482  uniioombllem3a  25483  uniioombllem3  25484  uniioombllem4  25485  uniioombllem6  25487  itgioo  25715  limcnlp  25777  dvbsss  25801  dvcnvrelem1  25920  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  pserdv  26337  rlimcnp2  26874  fsumharmonic  26920  chpval2  27127  bday0b  27744  madef  27766  madess  27790  oldssmade  27791  oldss  27792  n0sbday  28249  bdayn0p1  28263  tglnssp  28497  perpln1  28655  perpln2  28656  uhgrspansubgr  29236  clwwlknclwwlkdifnum  29924  ocsh  31227  shsss  31257  speccl  31843  elnlfn  31872  pj3i  32152  sumdmdlem2  32363  fcoinver  32548  ffsrn  32672  ssnnssfz  32730  pfxrn2  32881  ccatws1f1o  32893  cycpmrn  33085  cycpmconjslem2  33097  fxpss  33108  inftmrel  33122  ressply1mon1p  33503  ressply1invg  33504  evls1subd  33507  algextdeglem7  33690  algextdeglem8  33691  smatrcl  33763  metidss  33858  fsumcvg4  33917  dya2iocuni  34251  carsgcl  34272  breprexplema  34598  bnj1143  34757  bnj1262  34777  bnj517  34852  kur14lem1  35179  cvmliftmolem2  35255  cvmliftlem15  35271  mrsubrn  35486  msubrn  35502  poimirlem30  37630  mblfinlem2  37638  sdclem2  37722  sstotbnd2  37754  isbnd3  37764  lkrlss  39074  pmapssat  39738  diass  41021  diaintclN  41037  dia2dimlem13  41055  dibintclN  41146  lcfrlem25  41546  lcdvbasess  41573  mapdin  41641  mplsubrgcl  42521  diophin  42745  rmxyelqirr  42883  itgocn  43137  oaabsb  43267  oege1  43279  oege2  43280  oacl2g  43303  tfsconcatb0  43317  ofoafg  43327  ofoaf  43328  fpwfvss  43385  relexp0a  43689  frege131d  43737  fsovrfovd  43982  clsk1indlem2  44015  clsk1indlem3  44016  mnuprd  44249  unirestss  45102  founiiun0  45168  fsumsupp0  45559  limsupequzlem  45703  dvnprodlem1  45927  ibliooicc  45952  stoweidlem34  46015  stoweidlem59  46040  etransclem24  46239  caratheodory  46509  ovnhoilem1  46582  hspdifhsp  46597  smfaddlem2  46745  smflimlem1  46752  smflimlem2  46753  smfmullem4  46775  smfsuplem1  46792  fcoreslem4  47050  fcoresf1  47053  fcoresfo  47055  dfnbgrss  47836  dfnbgrss2  47843  isubgrsubgr  47853  rngchomrnghmresALTV  48263  rngcrescrhmALTV  48264  rhmsubcALTVlem1  48265  funcringcsetcALTV2lem9  48282  ssnn0ssfz  48333  isclatd  48967  nelsubclem  49052  setrec2fun  49677  setrec2mpt  49682