Theorem eqsstrdi 3975

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  eqsstrrdi  3976  eqimssd  3987  dmxpss  6164  dmsnopss  6210  iotassuni  6508  fvmptss  6999  fvmptss2  7013  funressn  7156  riotassuni  7410  ordsuci  7807  frxp  8124  suppssdm  8175  suppun  8182  suppss  8192  suppssov1  8195  suppssov2  8196  suppss2  8198  suppssfv  8200  oawordeulem  8541  omwordri  8559  oewordri  8580  mapssfset  8852  fodomr  9126  fodomfir  9297  fipwuni  9396  fipwss  9399  ordtypelem6  9495  inf3lemd  9606  cantnfle  9650  cantnflem2  9669  ttrclselem1  9704  en2other2  10012  ackbij1lem15  10235  ackbij2lem3  10242  cfub  10250  cflecard  10254  cfle  10255  fin23lem13  10334  fin23lem29  10343  compsscnvlem  10372  itunitc1  10422  fpwwe2lem11  10650  grur1a  10828  uzssz  12908  fsuppmapnn0fiublem  14054  fsuppmapnn0fiub  14055  swrdlend  14723  repswswrd  14855  cshimadifsn  14900  xptrrel  15053  relexpnndm  15114  relexpdmd  15117  relexprnd  15121  relexpfldd  15123  rtrclreclem4  15134  limsupgle  15564  isercolllem2  15753  isercolllem3  15754  isercoll  15755  fsumss  15811  sadcaddlem  16547  sadadd2lem  16549  sadadd3  16551  sadcl  16552  sadaddlem  16556  sadasslem  16560  sadeq  16562  smupvallem  16573  smucl  16574  prmreclem4  17011  prmreclem5  17012  1arith  17019  vdwmc2  17071  vdwlem13  17085  ramz2  17116  strfvss  17279  ressbasssg  17329  ressbasssOLD  17332  prdsless  17548  sectss  17841  invss  17850  fullfunc  17997  fthfunc  17998  catccatid  18195  resscatc  18198  catcisolem  18199  catciso  18200  yoniso  18373  gsumpropd2lem  18781  cntzrcl  19454  cntzssv  19455  gsumzmhm  20064  ablfaclem3  20216  rnghmresfn  20781  dfrngc2  20790  rnghmsscmap2  20791  rnghmsscmap  20792  funcrngcsetc  20802  rhmresfn  20810  dfringc2  20819  rhmsscmap2  20820  rhmsscmap  20821  rhmsscrnghm  20827  funcringcsetc  20836  rngcrescrhm  20846  rhmsubclem1  20847  rhmsubclem4  20850  lmhmlsp  21233  evpmss  21799  cssss  21898  frlmplusgval  21977  frlmvscafval  21979  uvcresum  22006  resspsrbas  22188  resspsrvsca  22191  subrgpsr  22192  mplsubglem  22213  ressmplbas  22243  subrgmpl  22247  mplsubrgcl  22248  opsrtoslem2  22272  mpfrcl  22301  ressply1bas  22453  ressply1evl  22595  evls1addd  22596  evls1muld  22597  evls1vsca  22598  evls1fvcl  22600  evls1maprhm  22601  scmatlss  22747  cpmatsubgpmat  22945  toponsspwpw  23147  basdif0  23178  ntrss2  23282  ordtbas2  23416  ordtbas  23417  cncls  23499  cmpfi  23633  comppfsc  23758  kgentopon  23764  ptpjpre1  23797  xkoccn  23845  prdstopn  23854  uzfbas  24124  utoptop  24460  utopbas  24461  setsmstopn  24704  restmetu  24796  tngtopn  24876  iccntr  25048  metdstri  25078  pi1xfrcnvlem  25284  cphsubrglem  25405  tcphcph  25465  rrxnm  25619  rrxbasefi  25638  ovolshftlem1  25737  ovolshft  25739  ovolscalem1  25741  ovolscalem2  25742  ovolsca  25743  uniioombllem2  25811  uniioombllem3a  25812  uniioombllem3  25813  uniioombllem4  25814  uniioombllem6  25816  itgioo  26043  limcnlp  26105  dvbsss  26129  dvcnvrelem1  26244  dvfsumle  26248  dvfsumabs  26250  pserdv  26665  rlimcnp2  27203  fsumharmonic  27248  chpval2  27454  bday0b  28078  madef  28101  madess  28131  oldssmade  28132  oldss  28135  n0bday  28617  bdayn0p1  28634  bdaypw2n0bndlem  28728  bdaypw2n0bnd  28729  tglnssp  28894  perpln1  29064  perpln2  29065  cgrabasimass  29257  uhgrspansubgr  29751  clwwlknclwwlkdifnum  30450  ocsh  31764  shsss  31794  speccl  32380  elnlfn  32409  pj3i  32689  sumdmdlem2  32900  fcoinver  33077  ffsrn  33199  ssnnssfz  33258  pfxrn2  33386  ccatws1f1o  33393  cycpmrn  33583  cycpmconjslem2  33595  fxpss  33606  inftmrel  33620  ressply1mon1p  33978  ressply1invg  33979  evls1subd  33982  esplyind  34085  algextdeglem7  34233  algextdeglem8  34234  smatrcl  34306  metidss  34401  fsumcvg4  34460  dya2iocuni  34794  carsgcl  34815  breprexplema  35138  bnj1143  35299  bnj1262  35319  bnj517  35394  kur14lem1  35785  cvmliftmolem2  35861  cvmliftlem15  35877  mrsubrn  36092  msubrn  36108  dfttc2g  37125  poimirlem30  38399  mblfinlem2  38407  sdclem2  38492  sstotbnd2  38524  isbnd3  38534  lkrlss  39968  pmapssat  40632  diass  41915  diaintclN  41931  dia2dimlem13  41949  dibintclN  42040  lcfrlem25  42440  lcdvbasess  42467  mapdin  42535  diophin  43617  rmxyelqirr  43751  itgocn  44005  oaabsb  44135  oege1  44147  oege2  44148  oacl2g  44171  tfsconcatb0  44185  ofoafg  44195  ofoaf  44196  fpwfvss  44252  relexp0a  44556  frege131d  44604  fsovrfovd  44849  clsk1indlem2  44882  clsk1indlem3  44883  mnuprd  45100  unirestss  45956  founiiun0  46022  fsumsupp0  46408  limsupequzlem  46550  dvnprodlem1  46774  ibliooicc  46799  stoweidlem34  46862  stoweidlem59  46887  etransclem24  47086  caratheodory  47356  ovnhoilem1  47429  hspdifhsp  47444  sssmf  47566  smfaddlem2  47592  smflimlem1  47599  smflimlem2  47600  smfmullem4  47622  smfsuplem1  47639  fcoreslem4  47954  fcoresf1  47957  fcoresfo  47959  dfnbgrss  48768  dfnbgrss2  48775  isubgrsubgr  48785  rngchomrnghmresALTV  49194  rngcrescrhmALTV  49195  rhmsubcALTVlem1  49196  funcringcsetcALTV2lem9  49213  ssnn0ssfz  49279  isclatd  49909  nelsubclem  49993  setrec2fun  50618  setrec2mpt  50623