Theorem eqsstrdi 3988

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3911

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 3928

This theorem is referenced by:  eqsstrrdi  3989  eqimssd  4000  dmxpss  6132  dmsnopss  6175  iotassuni  6471  iotassuniOLD  6478  fvmptss  6962  fvmptss2  6976  funressn  7113  riotassuni  7366  ordsuci  7764  frxp  8082  suppssdm  8133  suppun  8140  suppss  8150  suppssov1  8153  suppssov2  8154  suppss2  8156  suppssfv  8158  oawordeulem  8495  omwordri  8513  oewordri  8533  mapssfset  8801  fodomr  9069  fodomfir  9255  fipwuni  9353  fipwss  9356  ordtypelem6  9452  inf3lemd  9556  cantnfle  9600  cantnflem2  9619  ttrclselem1  9654  en2other2  9938  ackbij1lem15  10162  ackbij2lem3  10169  cfub  10178  cflecard  10182  cfle  10183  fin23lem13  10261  fin23lem29  10270  compsscnvlem  10299  itunitc1  10349  fpwwe2lem11  10570  grur1a  10748  uzssz  12790  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  swrdlend  14594  repswswrd  14725  cshimadifsn  14771  xptrrel  14922  relexpnndm  14983  relexpdmd  14986  relexprnd  14990  relexpfldd  14992  rtrclreclem4  15003  limsupgle  15419  isercolllem2  15608  isercolllem3  15609  isercoll  15610  fsumss  15667  sadcaddlem  16403  sadadd2lem  16405  sadadd3  16407  sadcl  16408  sadaddlem  16412  sadasslem  16416  sadeq  16418  smupvallem  16429  smucl  16430  prmreclem4  16866  prmreclem5  16867  1arith  16874  vdwmc2  16926  vdwlem13  16940  ramz2  16971  strfvss  17133  ressbasssg  17183  ressbasssOLD  17186  prdsless  17402  sectss  17690  invss  17699  fullfunc  17846  fthfunc  17847  catccatid  18044  resscatc  18047  catcisolem  18048  catciso  18049  yoniso  18222  gsumpropd2lem  18582  cntzrcl  19235  cntzssv  19236  gsumzmhm  19843  ablfaclem3  19995  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  20932  evpmss  21471  cssss  21570  frlmplusgval  21649  frlmvscafval  21651  uvcresum  21678  resspsrbas  21859  resspsrvsca  21862  subrgpsr  21863  mplsubglem  21884  ressmplbas  21911  subrgmpl  21915  opsrtoslem2  21939  mpfrcl  21968  ressply1bas  22089  ressply1evl  22233  evls1addd  22234  evls1muld  22235  evls1vsca  22236  evls1fvcl  22238  evls1maprhm  22239  scmatlss  22388  cpmatsubgpmat  22583  toponsspwpw  22785  basdif0  22816  ntrss2  22920  ordtbas2  23054  ordtbas  23055  cncls  23137  cmpfi  23271  comppfsc  23395  kgentopon  23401  ptpjpre1  23434  xkoccn  23482  prdstopn  23491  uzfbas  23761  utoptop  24098  utopbas  24099  setsmstopn  24342  restmetu  24434  tngtopn  24514  iccntr  24686  metdstri  24716  pi1xfrcnvlem  24932  cphsubrglem  25053  tcphcph  25113  rrxnm  25267  rrxbasefi  25286  ovolshftlem1  25386  ovolshft  25388  ovolscalem1  25390  ovolscalem2  25391  ovolsca  25392  uniioombllem2  25460  uniioombllem3a  25461  uniioombllem3  25462  uniioombllem4  25463  uniioombllem6  25465  itgioo  25693  limcnlp  25755  dvbsss  25779  dvcnvrelem1  25898  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  pserdv  26315  rlimcnp2  26852  fsumharmonic  26898  chpval2  27105  bday0b  27718  madef  27740  madess  27764  oldssmade  27765  n0sbday  28220  bdayn0p1  28234  tglnssp  28455  perpln1  28613  perpln2  28614  uhgrspansubgr  29194  clwwlknclwwlkdifnum  29882  ocsh  31185  shsss  31215  speccl  31801  elnlfn  31830  pj3i  32110  sumdmdlem2  32321  fcoinver  32506  ffsrn  32625  ssnnssfz  32683  pfxrn2  32834  ccatws1f1o  32846  cycpmrn  33073  cycpmconjslem2  33085  fxpss  33096  inftmrel  33107  ressply1mon1p  33510  ressply1invg  33511  evls1subd  33514  algextdeglem7  33686  algextdeglem8  33687  smatrcl  33759  metidss  33854  fsumcvg4  33913  dya2iocuni  34247  carsgcl  34268  breprexplema  34594  bnj1143  34753  bnj1262  34773  bnj517  34848  kur14lem1  35166  cvmliftmolem2  35242  cvmliftlem15  35258  mrsubrn  35473  msubrn  35489  poimirlem30  37617  mblfinlem2  37625  sdclem2  37709  sstotbnd2  37741  isbnd3  37751  lkrlss  39061  pmapssat  39726  diass  41009  diaintclN  41025  dia2dimlem13  41043  dibintclN  41134  lcfrlem25  41534  lcdvbasess  41561  mapdin  41629  mplsubrgcl  42509  diophin  42733  rmxyelqirr  42871  itgocn  43126  oaabsb  43256  oege1  43268  oege2  43269  oacl2g  43292  tfsconcatb0  43306  ofoafg  43316  ofoaf  43317  fpwfvss  43374  relexp0a  43678  frege131d  43726  fsovrfovd  43971  clsk1indlem2  44004  clsk1indlem3  44005  mnuprd  44238  unirestss  45091  founiiun0  45157  fsumsupp0  45549  limsupequzlem  45693  dvnprodlem1  45917  ibliooicc  45942  stoweidlem34  46005  stoweidlem59  46030  etransclem24  46229  caratheodory  46499  ovnhoilem1  46572  hspdifhsp  46587  smfaddlem2  46735  smflimlem1  46742  smflimlem2  46743  smfmullem4  46765  smfsuplem1  46782  fcoreslem4  47040  fcoresf1  47043  fcoresfo  47045  dfnbgrss  47825  dfnbgrss2  47832  isubgrsubgr  47842  rngchomrnghmresALTV  48240  rngcrescrhmALTV  48241  rhmsubcALTVlem1  48242  funcringcsetcALTV2lem9  48259  ssnn0ssfz  48310  isclatd  48944  nelsubclem  49029  setrec2fun  49654  setrec2mpt  49659