Theorem eqsstrdi 4035

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  eqsstrrdi  4036  eqimssd  4037  dmxpss  6169  dmsnopss  6212  iotassuni  6514  iotassuniOLD  6521  fvmptss  7009  fvmptss2  7022  fimacnvOLD  7071  funressn  7158  riotassuni  7408  ordsuci  7798  frxp  8114  suppssdm  8164  suppun  8171  suppss  8181  suppssOLD  8182  suppssov1  8185  suppss2  8187  suppssfv  8189  wfrlem15OLD  8325  oawordeulem  8556  omwordri  8574  oewordri  8594  mapssfset  8847  fodomr  9130  fipwuni  9423  fipwss  9426  ordtypelem6  9520  inf3lemd  9624  cantnfle  9668  cantnflem2  9687  ttrclselem1  9722  en2other2  10006  ackbij1lem15  10231  ackbij2lem3  10238  cfub  10246  cflecard  10250  cfle  10251  fin23lem13  10329  fin23lem29  10338  compsscnvlem  10367  itunitc1  10417  fpwwe2lem11  10638  grur1a  10816  uzssz  12847  fsuppmapnn0fiublem  13959  fsuppmapnn0fiub  13960  swrdlend  14607  repswswrd  14738  cshimadifsn  14784  xptrrel  14931  relexpnndm  14992  relexpdmd  14995  relexprnd  14999  relexpfldd  15001  rtrclreclem4  15012  limsupgle  15425  isercolllem2  15616  isercolllem3  15617  isercoll  15618  fsumss  15675  sadcaddlem  16402  sadadd2lem  16404  sadadd3  16406  sadcl  16407  sadaddlem  16411  sadasslem  16415  sadeq  16417  smupvallem  16428  smucl  16429  prmreclem4  16856  prmreclem5  16857  1arith  16864  vdwmc2  16916  vdwlem13  16930  ramz2  16961  strfvss  17124  ressbasssg  17185  ressbasssOLD  17188  prdsless  17413  sectss  17703  invss  17712  fullfunc  17861  fthfunc  17862  catccatid  18060  resscatc  18063  catcisolem  18064  catciso  18065  yoniso  18242  gsumpropd2lem  18604  cntzrcl  19232  cntzssv  19233  gsumzmhm  19846  ablfaclem3  19998  lmhmlsp  20804  evpmss  21358  cssss  21457  frlmplusgval  21538  frlmvscafval  21540  uvcresum  21567  resspsrbas  21754  resspsrvsca  21757  subrgpsr  21758  mplsubglem  21777  ressmplbas  21802  subrgmpl  21806  mpfrcl  21867  ressply1bas  21971  scmatlss  22247  cpmatsubgpmat  22442  toponsspwpw  22644  basdif0  22676  ntrss2  22781  ordtbas2  22915  ordtbas  22916  cncls  22998  cmpfi  23132  comppfsc  23256  kgentopon  23262  ptpjpre1  23295  xkoccn  23343  prdstopn  23352  uzfbas  23622  utoptop  23959  utopbas  23960  setsmstopn  24206  restmetu  24299  tngtopn  24387  iccntr  24557  metdstri  24587  pi1xfrcnvlem  24803  cphsubrglem  24925  tcphcph  24985  rrxnm  25139  rrxbasefi  25158  ovolshftlem1  25258  ovolshft  25260  ovolscalem1  25262  ovolscalem2  25263  ovolsca  25264  uniioombllem2  25332  uniioombllem3a  25333  uniioombllem3  25334  uniioombllem4  25335  uniioombllem6  25337  itgioo  25565  limcnlp  25627  dvbsss  25651  dvcnvrelem1  25769  dvfsumle  25773  dvfsumabs  25775  pserdv  26177  rlimcnp2  26707  fsumharmonic  26752  chpval2  26957  bday0b  27568  madef  27588  madess  27608  oldssmade  27609  tglnssp  28070  perpln1  28228  perpln2  28229  uhgrspansubgr  28815  clwwlknclwwlkdifnum  29500  ocsh  30803  shsss  30833  speccl  31419  elnlfn  31448  pj3i  31728  sumdmdlem2  31939  fcoinver  32102  ffsrn  32221  ssnnssfz  32265  pfxrn2  32373  cycpmrn  32572  cycpmconjslem2  32584  inftmrel  32596  ressply1evl  32921  evls1addd  32922  evls1muld  32923  evls1vsca  32924  ressply1mon1p  32931  ressply1invg  32932  evls1fvcl  33047  evls1maprhm  33048  algextdeglem7  33068  algextdeglem8  33069  smatrcl  33074  metidss  33169  fsumcvg4  33228  dya2iocuni  33580  carsgcl  33601  breprexplema  33940  bnj1143  34099  bnj1262  34119  bnj517  34194  kur14lem1  34495  cvmliftmolem2  34571  cvmliftlem15  34587  mrsubrn  34802  msubrn  34818  gg-dvfsumle  35468  poimirlem30  36821  mblfinlem2  36829  sdclem2  36913  sstotbnd2  36945  isbnd3  36955  lkrlss  38268  pmapssat  38933  diass  40216  diaintclN  40232  dia2dimlem13  40250  dibintclN  40341  lcfrlem25  40741  lcdvbasess  40768  mapdin  40836  mplsubrgcl  41421  diophin  41812  rmxyelqirr  41950  itgocn  42208  oaabsb  42346  oege1  42358  oege2  42359  oacl2g  42382  tfsconcatb0  42396  ofoafg  42406  ofoaf  42407  fpwfvss  42465  relexp0a  42769  frege131d  42817  fsovrfovd  43062  clsk1indlem2  43095  clsk1indlem3  43096  mnuprd  43337  unirestss  44114  founiiun0  44187  fsumsupp0  44592  limsupequzlem  44736  ibliooicc  44985  stoweidlem34  45048  stoweidlem59  45073  etransclem24  45272  caratheodory  45542  ovnhoilem1  45615  hspdifhsp  45630  smfaddlem2  45778  smflimlem1  45785  smflimlem2  45786  smfmullem4  45808  smfsuplem1  45825  fcoreslem4  46074  fcoresf1  46077  fcoresfo  46079  rnghmresfn  46949  dfrngc2  46958  rnghmsscmap2  46959  rnghmsscmap  46960  rngchomrnghmresALTV  46982  funcrngcsetc  46984  rhmresfn  46995  dfringc2  47004  rhmsscmap2  47005  rhmsscmap  47006  rhmsscrnghm  47012  funcringcsetc  47021  funcringcsetcALTV2lem9  47030  rngcrescrhm  47071  rhmsubclem1  47072  rhmsubclem4  47075  rngcrescrhmALTV  47089  rhmsubcALTVlem1  47090  ssnn0ssfz  47113  isclatd  47695  setrec2fun  47824  setrec2mpt  47829