Theorem eqsstrdi 3967

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  eqsstrrdi  3968  eqimssd  3979  dmxpss  6130  dmsnopss  6173  iotassuni  6468  fvmptss  6955  fvmptss2  6969  funressn  7107  riotassuni  7358  ordsuci  7756  frxp  8070  suppssdm  8121  suppun  8128  suppss  8138  suppssov1  8141  suppssov2  8142  suppss2  8144  suppssfv  8146  oawordeulem  8483  omwordri  8501  oewordri  8522  mapssfset  8792  fodomr  9060  fodomfir  9232  fipwuni  9333  fipwss  9336  ordtypelem6  9432  inf3lemd  9542  cantnfle  9586  cantnflem2  9605  ttrclselem1  9640  en2other2  9925  ackbij1lem15  10149  ackbij2lem3  10156  cfub  10165  cflecard  10169  cfle  10170  fin23lem13  10248  fin23lem29  10257  compsscnvlem  10286  itunitc1  10336  fpwwe2lem11  10558  grur1a  10736  uzssz  12803  fsuppmapnn0fiublem  13946  fsuppmapnn0fiub  13947  swrdlend  14610  repswswrd  14740  cshimadifsn  14785  xptrrel  14936  relexpnndm  14997  relexpdmd  15000  relexprnd  15004  relexpfldd  15006  rtrclreclem4  15017  limsupgle  15433  isercolllem2  15622  isercolllem3  15623  isercoll  15624  fsumss  15681  sadcaddlem  16420  sadadd2lem  16422  sadadd3  16424  sadcl  16425  sadaddlem  16429  sadasslem  16433  sadeq  16435  smupvallem  16446  smucl  16447  prmreclem4  16884  prmreclem5  16885  1arith  16892  vdwmc2  16944  vdwlem13  16958  ramz2  16989  strfvss  17151  ressbasssg  17201  ressbasssOLD  17204  prdsless  17420  sectss  17713  invss  17722  fullfunc  17869  fthfunc  17870  catccatid  18067  resscatc  18070  catcisolem  18071  catciso  18072  yoniso  18245  gsumpropd2lem  18641  cntzrcl  19296  cntzssv  19297  gsumzmhm  19906  ablfaclem3  20058  rnghmresfn  20590  dfrngc2  20599  rnghmsscmap2  20600  rnghmsscmap  20601  funcrngcsetc  20611  rhmresfn  20619  dfringc2  20628  rhmsscmap2  20629  rhmsscmap  20630  rhmsscrnghm  20636  funcringcsetc  20645  rngcrescrhm  20655  rhmsubclem1  20656  rhmsubclem4  20659  lmhmlsp  21039  evpmss  21579  cssss  21678  frlmplusgval  21757  frlmvscafval  21759  uvcresum  21786  resspsrbas  21965  resspsrvsca  21968  subrgpsr  21969  mplsubglem  21990  ressmplbas  22019  subrgmpl  22023  opsrtoslem2  22047  mpfrcl  22076  ressply1bas  22205  ressply1evl  22348  evls1addd  22349  evls1muld  22350  evls1vsca  22351  evls1fvcl  22353  evls1maprhm  22354  scmatlss  22503  cpmatsubgpmat  22698  toponsspwpw  22900  basdif0  22931  ntrss2  23035  ordtbas2  23169  ordtbas  23170  cncls  23252  cmpfi  23386  comppfsc  23510  kgentopon  23516  ptpjpre1  23549  xkoccn  23597  prdstopn  23606  uzfbas  23876  utoptop  24212  utopbas  24213  setsmstopn  24456  restmetu  24548  tngtopn  24628  iccntr  24800  metdstri  24830  pi1xfrcnvlem  25036  cphsubrglem  25157  tcphcph  25217  rrxnm  25371  rrxbasefi  25390  ovolshftlem1  25489  ovolshft  25491  ovolscalem1  25493  ovolscalem2  25494  ovolsca  25495  uniioombllem2  25563  uniioombllem3a  25564  uniioombllem3  25565  uniioombllem4  25566  uniioombllem6  25568  itgioo  25796  limcnlp  25858  dvbsss  25882  dvcnvrelem1  25997  dvfsumle  26001  dvfsumabs  26003  pserdv  26410  rlimcnp2  26946  fsumharmonic  26992  chpval2  27198  bday0b  27822  madef  27845  madess  27875  oldssmade  27876  oldss  27879  n0bday  28361  bdayn0p1  28378  bdaypw2n0bndlem  28472  bdaypw2n0bnd  28473  tglnssp  28637  perpln1  28795  perpln2  28796  uhgrspansubgr  29377  clwwlknclwwlkdifnum  30068  ocsh  31372  shsss  31402  speccl  31988  elnlfn  32017  pj3i  32297  sumdmdlem2  32508  fcoinver  32692  ffsrn  32819  ssnnssfz  32878  pfxrn2  33018  ccatws1f1o  33029  cycpmrn  33222  cycpmconjslem2  33234  fxpss  33245  inftmrel  33259  ressply1mon1p  33646  ressply1invg  33647  evls1subd  33650  esplyind  33737  algextdeglem7  33886  algextdeglem8  33887  smatrcl  33959  metidss  34054  fsumcvg4  34113  dya2iocuni  34446  carsgcl  34467  breprexplema  34793  bnj1143  34951  bnj1262  34971  bnj517  35046  kur14lem1  35407  cvmliftmolem2  35483  cvmliftlem15  35499  mrsubrn  35714  msubrn  35730  dfttc2g  36707  poimirlem30  37988  mblfinlem2  37996  sdclem2  38080  sstotbnd2  38112  isbnd3  38122  lkrlss  39558  pmapssat  40222  diass  41505  diaintclN  41521  dia2dimlem13  41539  dibintclN  41630  lcfrlem25  42030  lcdvbasess  42057  mapdin  42125  mplsubrgcl  43008  diophin  43221  rmxyelqirr  43359  itgocn  43613  oaabsb  43743  oege1  43755  oege2  43756  oacl2g  43779  tfsconcatb0  43793  ofoafg  43803  ofoaf  43804  fpwfvss  43860  relexp0a  44164  frege131d  44212  fsovrfovd  44457  clsk1indlem2  44490  clsk1indlem3  44491  mnuprd  44724  unirestss  45575  founiiun0  45641  fsumsupp0  46029  limsupequzlem  46171  dvnprodlem1  46395  ibliooicc  46420  stoweidlem34  46483  stoweidlem59  46508  etransclem24  46707  caratheodory  46977  ovnhoilem1  47050  hspdifhsp  47065  smfaddlem2  47213  smflimlem1  47220  smflimlem2  47221  smfmullem4  47243  smfsuplem1  47260  fcoreslem4  47529  fcoresf1  47532  fcoresfo  47534  dfnbgrss  48343  dfnbgrss2  48350  isubgrsubgr  48360  rngchomrnghmresALTV  48770  rngcrescrhmALTV  48771  rhmsubcALTVlem1  48772  funcringcsetcALTV2lem9  48789  ssnn0ssfz  48840  isclatd  49473  nelsubclem  49557  setrec2fun  50182  setrec2mpt  50187