Theorem eqsstrdi 3982

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  eqsstrrdi  3983  eqimssd  3994  dmxpss  6171  dmsnopss  6217  iotassuni  6515  fvmptss  7006  fvmptss2  7020  funressn  7162  riotassuni  7416  ordsuci  7813  frxp  8128  suppssdm  8179  suppun  8186  suppss  8196  suppssov1  8199  suppssov2  8200  suppss2  8202  suppssfv  8204  oawordeulem  8545  omwordri  8563  oewordri  8584  mapssfset  8854  fodomr  9123  fodomfir  9294  fipwuni  9393  fipwss  9396  ordtypelem6  9492  inf3lemd  9603  cantnfle  9647  cantnflem2  9666  ttrclselem1  9701  en2other2  10009  ackbij1lem15  10232  ackbij2lem3  10239  cfub  10247  cflecard  10251  cfle  10252  fin23lem13  10331  fin23lem29  10340  compsscnvlem  10369  itunitc1  10419  fpwwe2lem11  10641  grur1a  10819  uzssz  12899  fsuppmapnn0fiublem  14044  fsuppmapnn0fiub  14045  swrdlend  14713  repswswrd  14845  cshimadifsn  14890  xptrrel  15041  relexpnndm  15102  relexpdmd  15105  relexprnd  15109  relexpfldd  15111  rtrclreclem4  15122  limsupgle  15552  isercolllem2  15741  isercolllem3  15742  isercoll  15743  fsumss  15799  sadcaddlem  16537  sadadd2lem  16539  sadadd3  16541  sadcl  16542  sadaddlem  16546  sadasslem  16550  sadeq  16552  smupvallem  16563  smucl  16564  prmreclem4  17001  prmreclem5  17002  1arith  17009  vdwmc2  17061  vdwlem13  17075  ramz2  17106  strfvss  17269  ressbasssg  17319  ressbasssOLD  17322  prdsless  17538  sectss  17831  invss  17840  fullfunc  17987  fthfunc  17988  catccatid  18185  resscatc  18188  catcisolem  18189  catciso  18190  yoniso  18363  gsumpropd2lem  18769  cntzrcl  19441  cntzssv  19442  gsumzmhm  20051  ablfaclem3  20203  rnghmresfn  20768  dfrngc2  20777  rnghmsscmap2  20778  rnghmsscmap  20779  funcrngcsetc  20789  rhmresfn  20797  dfringc2  20806  rhmsscmap2  20807  rhmsscmap  20808  rhmsscrnghm  20814  funcringcsetc  20823  rngcrescrhm  20833  rhmsubclem1  20834  rhmsubclem4  20837  lmhmlsp  21220  evpmss  21786  cssss  21885  frlmplusgval  21964  frlmvscafval  21966  uvcresum  21993  resspsrbas  22173  resspsrvsca  22176  subrgpsr  22177  mplsubglem  22198  ressmplbas  22228  subrgmpl  22232  mplsubrgcl  22233  opsrtoslem2  22257  mpfrcl  22286  ressply1bas  22438  ressply1evl  22580  evls1addd  22581  evls1muld  22582  evls1vsca  22583  evls1fvcl  22585  evls1maprhm  22586  scmatlss  22732  cpmatsubgpmat  22927  toponsspwpw  23129  basdif0  23160  ntrss2  23264  ordtbas2  23398  ordtbas  23399  cncls  23481  cmpfi  23615  comppfsc  23740  kgentopon  23746  ptpjpre1  23779  xkoccn  23827  prdstopn  23836  uzfbas  24106  utoptop  24442  utopbas  24443  setsmstopn  24686  restmetu  24778  tngtopn  24858  iccntr  25030  metdstri  25060  pi1xfrcnvlem  25266  cphsubrglem  25387  tcphcph  25447  rrxnm  25601  rrxbasefi  25620  ovolshftlem1  25719  ovolshft  25721  ovolscalem1  25723  ovolscalem2  25724  ovolsca  25725  uniioombllem2  25793  uniioombllem3a  25794  uniioombllem3  25795  uniioombllem4  25796  uniioombllem6  25798  itgioo  26026  limcnlp  26088  dvbsss  26112  dvcnvrelem1  26227  dvfsumle  26231  dvfsumabs  26233  pserdv  26643  rlimcnp2  27182  fsumharmonic  27227  chpval2  27433  bday0b  28057  madef  28080  madess  28110  oldssmade  28111  oldss  28114  n0bday  28596  bdayn0p1  28613  bdaypw2n0bndlem  28707  bdaypw2n0bnd  28708  tglnssp  28872  perpln1  29041  perpln2  29042  uhgrspansubgr  29699  clwwlknclwwlkdifnum  30398  ocsh  31706  shsss  31736  speccl  32322  elnlfn  32351  pj3i  32631  sumdmdlem2  32842  fcoinver  33020  ffsrn  33143  ssnnssfz  33202  pfxrn2  33330  ccatws1f1o  33337  cycpmrn  33527  cycpmconjslem2  33539  fxpss  33550  inftmrel  33564  ressply1mon1p  33922  ressply1invg  33923  evls1subd  33926  esplyind  34029  algextdeglem7  34177  algextdeglem8  34178  smatrcl  34250  metidss  34345  fsumcvg4  34404  dya2iocuni  34738  carsgcl  34759  breprexplema  35082  bnj1143  35243  bnj1262  35263  bnj517  35338  kur14lem1  35735  cvmliftmolem2  35811  cvmliftlem15  35827  mrsubrn  36042  msubrn  36058  dfttc2g  37074  poimirlem30  38358  mblfinlem2  38366  sdclem2  38451  sstotbnd2  38483  isbnd3  38493  lkrlss  39927  pmapssat  40591  diass  41874  diaintclN  41890  dia2dimlem13  41908  dibintclN  41999  lcfrlem25  42399  lcdvbasess  42426  mapdin  42494  diophin  43561  rmxyelqirr  43695  itgocn  43949  oaabsb  44079  oege1  44091  oege2  44092  oacl2g  44115  tfsconcatb0  44129  ofoafg  44139  ofoaf  44140  fpwfvss  44196  relexp0a  44500  frege131d  44548  fsovrfovd  44793  clsk1indlem2  44826  clsk1indlem3  44827  mnuprd  45044  unirestss  45900  founiiun0  45966  fsumsupp0  46352  limsupequzlem  46494  dvnprodlem1  46718  ibliooicc  46743  stoweidlem34  46806  stoweidlem59  46831  etransclem24  47030  caratheodory  47300  ovnhoilem1  47373  hspdifhsp  47388  sssmf  47510  smfaddlem2  47536  smflimlem1  47543  smflimlem2  47544  smfmullem4  47566  smfsuplem1  47583  fcoreslem4  47861  fcoresf1  47864  fcoresfo  47866  dfnbgrss  48675  dfnbgrss2  48682  isubgrsubgr  48692  rngchomrnghmresALTV  49101  rngcrescrhmALTV  49102  rhmsubcALTVlem1  49103  funcringcsetcALTV2lem9  49120  ssnn0ssfz  49186  isclatd  49818  nelsubclem  49902  setrec2fun  50527  setrec2mpt  50532