Theorem eqsstrdi 4021

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  eqsstrrdi  4022  dmxpss  6028  dmsnopss  6071  iotassuni  6334  fvmptss  6780  fvmptss2  6793  fimacnv  6839  funressn  6921  riotassuni  7154  frxp  7820  suppssdm  7843  suppun  7850  suppss  7860  suppssov1  7862  suppss2  7864  suppssfv  7866  wfrlem15  7969  oawordeulem  8180  omwordri  8198  oewordri  8218  fodomr  8668  fipwuni  8890  fipwss  8893  ordtypelem6  8987  inf3lemd  9090  cantnfle  9134  cantnflem2  9153  en2other2  9435  ackbij1lem15  9656  ackbij2lem3  9663  cfub  9671  cflecard  9675  cfle  9676  fin23lem13  9754  fin23lem29  9763  compsscnvlem  9792  itunitc1  9842  fpwwe2lem12  10063  grur1a  10241  uzssz  12265  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  swrdlend  14015  repswswrd  14146  cshimadifsn  14191  xptrrel  14340  relexpnndm  14400  limsupgle  14834  isercolllem2  15022  isercolllem3  15023  isercoll  15024  fsumss  15082  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadcl  15811  sadaddlem  15815  sadasslem  15819  sadeq  15821  smupvallem  15832  smucl  15833  prmreclem4  16255  prmreclem5  16256  1arith  16263  vdwmc2  16315  vdwlem13  16329  ramz2  16360  strfvss  16506  ressbasss  16556  prdsless  16736  sectss  17022  invss  17031  fullfunc  17176  fthfunc  17177  catccatid  17362  resscatc  17365  catcisolem  17366  catciso  17367  yoniso  17535  gsumpropd2lem  17889  cntzrcl  18457  cntzssv  18458  gsumzmhm  19057  ablfaclem3  19209  lmhmlsp  19821  resspsrbas  20195  resspsrvsca  20198  subrgpsr  20199  mplsubglem  20214  ressmplbas  20237  subrgmpl  20241  mpfrcl  20298  mhp0cl  20337  ressply1bas  20397  evpmss  20730  cssss  20829  frlmplusgval  20908  frlmvscafval  20910  uvcresum  20937  scmatlss  21134  cpmatsubgpmat  21328  toponsspwpw  21530  basdif0  21561  ntrss2  21665  ordtbas2  21799  ordtbas  21800  cncls  21882  cmpfi  22016  comppfsc  22140  kgentopon  22146  ptpjpre1  22179  xkoccn  22227  prdstopn  22236  uzfbas  22506  utoptop  22843  utopbas  22844  setsmstopn  23088  restmetu  23180  tngtopn  23259  iccntr  23429  metdstri  23459  pi1xfrcnvlem  23660  cphsubrglem  23781  tcphcph  23840  rrxnm  23994  rrxbasefi  24013  ovolshftlem1  24110  ovolshft  24112  ovolscalem1  24114  ovolscalem2  24115  ovolsca  24116  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  itgioo  24416  limcnlp  24476  dvbsss  24500  dvcnvrelem1  24614  dvfsumle  24618  dvfsumabs  24620  pserdv  25017  rlimcnp2  25544  fsumharmonic  25589  chpval2  25794  tglnssp  26338  perpln1  26496  perpln2  26497  uhgrspansubgr  27073  clwwlknclwwlkdifnum  27758  ocsh  29060  shsss  29090  speccl  29676  elnlfn  29705  pj3i  29985  sumdmdlem2  30196  fcoinver  30357  ffsrn  30465  ssnnssfz  30510  pfxrn2  30616  cycpmrn  30785  cycpmconjslem2  30797  inftmrel  30809  smatrcl  31061  metidss  31131  fsumcvg4  31193  dya2iocuni  31541  carsgcl  31562  breprexplema  31901  bnj1143  32062  bnj1262  32082  bnj517  32157  kur14lem1  32453  cvmliftmolem2  32529  cvmliftlem15  32545  mrsubrn  32760  msubrn  32776  trpredlem1  33066  poimirlem30  34937  mblfinlem2  34945  sdclem2  35032  sstotbnd2  35067  isbnd3  35077  lkrlss  36246  pmapssat  36910  diass  38193  diaintclN  38209  dia2dimlem13  38227  dibintclN  38318  lcfrlem25  38718  lcdvbasess  38745  mapdin  38813  diophin  39418  itgocn  39813  relexp0a  40110  frege131d  40158  fsovrfovd  40404  clsk1indlem2  40441  clsk1indlem3  40442  mnuprd  40661  unirestss  41439  founiiun0  41500  fsumsupp0  41908  limsupequzlem  42052  ibliooicc  42305  stoweidlem34  42368  stoweidlem59  42393  etransclem24  42592  caratheodory  42859  ovnhoilem1  42932  hspdifhsp  42947  smfaddlem2  43089  smflimlem1  43096  smflimlem2  43097  smfmullem4  43118  smfsuplem1  43134  rnghmresfn  44283  dfrngc2  44292  rnghmsscmap2  44293  rnghmsscmap  44294  rngchomrnghmresALTV  44316  funcrngcsetc  44318  rhmresfn  44329  dfringc2  44338  rhmsscmap2  44339  rhmsscmap  44340  rhmsscrnghm  44346  funcringcsetc  44355  funcringcsetcALTV2lem9  44364  rngcrescrhm  44405  rhmsubclem1  44406  rhmsubclem4  44409  rngcrescrhmALTV  44423  rhmsubcALTVlem1  44424  ssnn0ssfz  44446  setrec2fun  44844