Theorem eqsstrdi 4032

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

Syntax hints:   → wi 4   = wceq 1534   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  eqsstrrdi  4033  eqimssd  4034  dmxpss  6169  dmsnopss  6212  iotassuni  6514  iotassuniOLD  6521  fvmptss  7011  fvmptss2  7025  fimacnvOLD  7074  funressn  7162  riotassuni  7411  ordsuci  7805  frxp  8125  suppssdm  8175  suppun  8182  suppss  8192  suppssOLD  8193  suppssov1  8196  suppssov2  8197  suppss2  8199  suppssfv  8201  wfrlem15OLD  8337  oawordeulem  8568  omwordri  8586  oewordri  8606  mapssfset  8861  fodomr  9144  fipwuni  9441  fipwss  9444  ordtypelem6  9538  inf3lemd  9642  cantnfle  9686  cantnflem2  9705  ttrclselem1  9740  en2other2  10024  ackbij1lem15  10249  ackbij2lem3  10256  cfub  10264  cflecard  10268  cfle  10269  fin23lem13  10347  fin23lem29  10356  compsscnvlem  10385  itunitc1  10435  fpwwe2lem11  10656  grur1a  10834  uzssz  12865  fsuppmapnn0fiublem  13979  fsuppmapnn0fiub  13980  swrdlend  14627  repswswrd  14758  cshimadifsn  14804  xptrrel  14951  relexpnndm  15012  relexpdmd  15015  relexprnd  15019  relexpfldd  15021  rtrclreclem4  15032  limsupgle  15445  isercolllem2  15636  isercolllem3  15637  isercoll  15638  fsumss  15695  sadcaddlem  16423  sadadd2lem  16425  sadadd3  16427  sadcl  16428  sadaddlem  16432  sadasslem  16436  sadeq  16438  smupvallem  16449  smucl  16450  prmreclem4  16879  prmreclem5  16880  1arith  16887  vdwmc2  16939  vdwlem13  16953  ramz2  16984  strfvss  17147  ressbasssg  17208  ressbasssOLD  17211  prdsless  17436  sectss  17726  invss  17735  fullfunc  17886  fthfunc  17887  catccatid  18086  resscatc  18089  catcisolem  18090  catciso  18091  yoniso  18268  gsumpropd2lem  18630  cntzrcl  19269  cntzssv  19270  gsumzmhm  19883  ablfaclem3  20035  rnghmresfn  20541  dfrngc2  20550  rnghmsscmap2  20551  rnghmsscmap  20552  funcrngcsetc  20562  rhmresfn  20570  dfringc2  20579  rhmsscmap2  20580  rhmsscmap  20581  rhmsscrnghm  20587  funcringcsetc  20596  rngcrescrhm  20606  rhmsubclem1  20607  rhmsubclem4  20610  lmhmlsp  20923  evpmss  21505  cssss  21604  frlmplusgval  21685  frlmvscafval  21687  uvcresum  21714  resspsrbas  21904  resspsrvsca  21907  subrgpsr  21908  mplsubglem  21928  ressmplbas  21953  subrgmpl  21957  mpfrcl  22018  ressply1bas  22134  scmatlss  22414  cpmatsubgpmat  22609  toponsspwpw  22811  basdif0  22843  ntrss2  22948  ordtbas2  23082  ordtbas  23083  cncls  23165  cmpfi  23299  comppfsc  23423  kgentopon  23429  ptpjpre1  23462  xkoccn  23510  prdstopn  23519  uzfbas  23789  utoptop  24126  utopbas  24127  setsmstopn  24373  restmetu  24466  tngtopn  24554  iccntr  24724  metdstri  24754  pi1xfrcnvlem  24970  cphsubrglem  25092  tcphcph  25152  rrxnm  25306  rrxbasefi  25325  ovolshftlem1  25425  ovolshft  25427  ovolscalem1  25429  ovolscalem2  25430  ovolsca  25431  uniioombllem2  25499  uniioombllem3a  25500  uniioombllem3  25501  uniioombllem4  25502  uniioombllem6  25504  itgioo  25732  limcnlp  25794  dvbsss  25818  dvcnvrelem1  25937  dvfsumle  25941  dvfsumleOLD  25942  dvfsumabs  25944  pserdv  26353  rlimcnp2  26885  fsumharmonic  26931  chpval2  27138  bday0b  27750  madef  27770  madess  27790  oldssmade  27791  n0sbday  28204  tglnssp  28343  perpln1  28501  perpln2  28502  uhgrspansubgr  29091  clwwlknclwwlkdifnum  29777  ocsh  31080  shsss  31110  speccl  31696  elnlfn  31725  pj3i  32005  sumdmdlem2  32216  fcoinver  32379  ffsrn  32495  ssnnssfz  32539  pfxrn2  32645  cycpmrn  32842  cycpmconjslem2  32854  inftmrel  32866  ressply1mon1p  33179  ressply1invg  33180  ressply1evl  33183  evls1addd  33184  evls1subd  33185  evls1muld  33186  evls1vsca  33187  evls1fvcl  33304  evls1maprhm  33305  algextdeglem7  33327  algextdeglem8  33328  smatrcl  33333  metidss  33428  fsumcvg4  33487  dya2iocuni  33839  carsgcl  33860  breprexplema  34198  bnj1143  34357  bnj1262  34377  bnj517  34452  kur14lem1  34752  cvmliftmolem2  34828  cvmliftlem15  34844  mrsubrn  35059  msubrn  35075  poimirlem30  37058  mblfinlem2  37066  sdclem2  37150  sstotbnd2  37182  isbnd3  37192  lkrlss  38504  pmapssat  39169  diass  40452  diaintclN  40468  dia2dimlem13  40486  dibintclN  40577  lcfrlem25  40977  lcdvbasess  41004  mapdin  41072  mplsubrgcl  41702  diophin  42114  rmxyelqirr  42252  itgocn  42510  oaabsb  42646  oege1  42658  oege2  42659  oacl2g  42682  tfsconcatb0  42696  ofoafg  42706  ofoaf  42707  fpwfvss  42765  relexp0a  43069  frege131d  43117  fsovrfovd  43362  clsk1indlem2  43395  clsk1indlem3  43396  mnuprd  43636  unirestss  44413  founiiun0  44486  fsumsupp0  44889  limsupequzlem  45033  ibliooicc  45282  stoweidlem34  45345  stoweidlem59  45370  etransclem24  45569  caratheodory  45839  ovnhoilem1  45912  hspdifhsp  45927  smfaddlem2  46075  smflimlem1  46082  smflimlem2  46083  smfmullem4  46105  smfsuplem1  46122  fcoreslem4  46371  fcoresf1  46374  fcoresfo  46376  rngchomrnghmresALTV  47264  rngcrescrhmALTV  47265  rhmsubcALTVlem1  47266  funcringcsetcALTV2lem9  47283  ssnn0ssfz  47336  isclatd  47917  setrec2fun  48046  setrec2mpt  48051