Theorem eqsstrdi 4036

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  eqsstrrdi  4037  eqimssd  4038  dmxpss  6170  dmsnopss  6213  iotassuni  6515  iotassuniOLD  6522  fvmptss  7010  fvmptss2  7023  fimacnvOLD  7072  funressn  7159  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  24796  cphsubrglem  24918  tcphcph  24978  rrxnm  25132  rrxbasefi  25151  ovolshftlem1  25250  ovolshft  25252  ovolscalem1  25254  ovolscalem2  25255  ovolsca  25256  uniioombllem2  25324  uniioombllem3a  25325  uniioombllem3  25326  uniioombllem4  25327  uniioombllem6  25329  itgioo  25557  limcnlp  25619  dvbsss  25643  dvcnvrelem1  25758  dvfsumle  25762  dvfsumabs  25764  pserdv  26165  rlimcnp2  26695  fsumharmonic  26740  chpval2  26945  bday0b  27556  madef  27576  madess  27596  oldssmade  27597  tglnssp  28058  perpln1  28216  perpln2  28217  uhgrspansubgr  28803  clwwlknclwwlkdifnum  29488  ocsh  30791  shsss  30821  speccl  31407  elnlfn  31436  pj3i  31716  sumdmdlem2  31927  fcoinver  32090  ffsrn  32209  ssnnssfz  32253  pfxrn2  32361  cycpmrn  32560  cycpmconjslem2  32572  inftmrel  32584  ressply1evl  32909  evls1addd  32910  evls1muld  32911  evls1vsca  32912  ressply1mon1p  32919  ressply1invg  32920  evls1fvcl  33035  evls1maprhm  33036  algextdeglem7  33056  algextdeglem8  33057  smatrcl  33062  metidss  33157  fsumcvg4  33216  dya2iocuni  33568  carsgcl  33589  breprexplema  33928  bnj1143  34087  bnj1262  34107  bnj517  34182  kur14lem1  34483  cvmliftmolem2  34559  cvmliftlem15  34575  mrsubrn  34790  msubrn  34806  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  44115  founiiun0  44188  fsumsupp0  44593  limsupequzlem  44737  ibliooicc  44986  stoweidlem34  45049  stoweidlem59  45074  etransclem24  45273  caratheodory  45543  ovnhoilem1  45616  hspdifhsp  45631  smfaddlem2  45779  smflimlem1  45786  smflimlem2  45787  smfmullem4  45809  smfsuplem1  45826  fcoreslem4  46075  fcoresf1  46078  fcoresfo  46080  rnghmresfn  46950  dfrngc2  46959  rnghmsscmap2  46960  rnghmsscmap  46961  rngchomrnghmresALTV  46983  funcrngcsetc  46985  rhmresfn  46996  dfringc2  47005  rhmsscmap2  47006  rhmsscmap  47007  rhmsscrnghm  47013  funcringcsetc  47022  funcringcsetcALTV2lem9  47031  rngcrescrhm  47072  rhmsubclem1  47073  rhmsubclem4  47076  rngcrescrhmALTV  47090  rhmsubcALTVlem1  47091  ssnn0ssfz  47114  isclatd  47696  setrec2fun  47825  setrec2mpt  47830