Theorem eqsstrdi 3978

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

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

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  eqsstrrdi  3979  eqimssd  3990  dmxpss  6129  dmsnopss  6172  iotassuni  6467  fvmptss  6953  fvmptss2  6967  funressn  7104  riotassuni  7355  ordsuci  7753  frxp  8068  suppssdm  8119  suppun  8126  suppss  8136  suppssov1  8139  suppssov2  8140  suppss2  8142  suppssfv  8144  oawordeulem  8481  omwordri  8499  oewordri  8520  mapssfset  8788  fodomr  9056  fodomfir  9228  fipwuni  9329  fipwss  9332  ordtypelem6  9428  inf3lemd  9536  cantnfle  9580  cantnflem2  9599  ttrclselem1  9634  en2other2  9919  ackbij1lem15  10143  ackbij2lem3  10150  cfub  10159  cflecard  10163  cfle  10164  fin23lem13  10242  fin23lem29  10251  compsscnvlem  10280  itunitc1  10330  fpwwe2lem11  10552  grur1a  10730  uzssz  12772  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  swrdlend  14577  repswswrd  14707  cshimadifsn  14752  xptrrel  14903  relexpnndm  14964  relexpdmd  14967  relexprnd  14971  relexpfldd  14973  rtrclreclem4  14984  limsupgle  15400  isercolllem2  15589  isercolllem3  15590  isercoll  15591  fsumss  15648  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadcl  16389  sadaddlem  16393  sadasslem  16397  sadeq  16399  smupvallem  16410  smucl  16411  prmreclem4  16847  prmreclem5  16848  1arith  16855  vdwmc2  16907  vdwlem13  16921  ramz2  16952  strfvss  17114  ressbasssg  17164  ressbasssOLD  17167  prdsless  17383  sectss  17676  invss  17685  fullfunc  17832  fthfunc  17833  catccatid  18030  resscatc  18033  catcisolem  18034  catciso  18035  yoniso  18208  gsumpropd2lem  18604  cntzrcl  19256  cntzssv  19257  gsumzmhm  19866  ablfaclem3  20018  rnghmresfn  20552  dfrngc2  20561  rnghmsscmap2  20562  rnghmsscmap  20563  funcrngcsetc  20573  rhmresfn  20581  dfringc2  20590  rhmsscmap2  20591  rhmsscmap  20592  rhmsscrnghm  20598  funcringcsetc  20607  rngcrescrhm  20617  rhmsubclem1  20618  rhmsubclem4  20621  lmhmlsp  21001  evpmss  21541  cssss  21640  frlmplusgval  21719  frlmvscafval  21721  uvcresum  21748  resspsrbas  21929  resspsrvsca  21932  subrgpsr  21933  mplsubglem  21954  ressmplbas  21983  subrgmpl  21987  opsrtoslem2  22011  mpfrcl  22040  ressply1bas  22169  ressply1evl  22314  evls1addd  22315  evls1muld  22316  evls1vsca  22317  evls1fvcl  22319  evls1maprhm  22320  scmatlss  22469  cpmatsubgpmat  22664  toponsspwpw  22866  basdif0  22897  ntrss2  23001  ordtbas2  23135  ordtbas  23136  cncls  23218  cmpfi  23352  comppfsc  23476  kgentopon  23482  ptpjpre1  23515  xkoccn  23563  prdstopn  23572  uzfbas  23842  utoptop  24178  utopbas  24179  setsmstopn  24422  restmetu  24514  tngtopn  24594  iccntr  24766  metdstri  24796  pi1xfrcnvlem  25012  cphsubrglem  25133  tcphcph  25193  rrxnm  25347  rrxbasefi  25366  ovolshftlem1  25466  ovolshft  25468  ovolscalem1  25470  ovolscalem2  25471  ovolsca  25472  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem6  25545  itgioo  25773  limcnlp  25835  dvbsss  25859  dvcnvrelem1  25978  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  pserdv  26395  rlimcnp2  26932  fsumharmonic  26978  chpval2  27185  bday0b  27809  madef  27832  madess  27862  oldssmade  27863  oldss  27866  n0bday  28348  bdayn0p1  28365  bdaypw2n0bndlem  28459  bdaypw2n0bnd  28460  tglnssp  28624  perpln1  28782  perpln2  28783  uhgrspansubgr  29364  clwwlknclwwlkdifnum  30055  ocsh  31358  shsss  31388  speccl  31974  elnlfn  32003  pj3i  32283  sumdmdlem2  32494  fcoinver  32679  ffsrn  32807  ssnnssfz  32867  pfxrn2  33022  ccatws1f1o  33033  cycpmrn  33225  cycpmconjslem2  33237  fxpss  33248  inftmrel  33262  ressply1mon1p  33649  ressply1invg  33650  evls1subd  33653  esplyind  33731  algextdeglem7  33880  algextdeglem8  33881  smatrcl  33953  metidss  34048  fsumcvg4  34107  dya2iocuni  34440  carsgcl  34461  breprexplema  34787  bnj1143  34946  bnj1262  34966  bnj517  35041  kur14lem1  35400  cvmliftmolem2  35476  cvmliftlem15  35492  mrsubrn  35707  msubrn  35723  poimirlem30  37851  mblfinlem2  37859  sdclem2  37943  sstotbnd2  37975  isbnd3  37985  lkrlss  39355  pmapssat  40019  diass  41302  diaintclN  41318  dia2dimlem13  41336  dibintclN  41427  lcfrlem25  41827  lcdvbasess  41854  mapdin  41922  mplsubrgcl  42801  diophin  43014  rmxyelqirr  43152  itgocn  43406  oaabsb  43536  oege1  43548  oege2  43549  oacl2g  43572  tfsconcatb0  43586  ofoafg  43596  ofoaf  43597  fpwfvss  43653  relexp0a  43957  frege131d  44005  fsovrfovd  44250  clsk1indlem2  44283  clsk1indlem3  44284  mnuprd  44517  unirestss  45368  founiiun0  45434  fsumsupp0  45824  limsupequzlem  45966  dvnprodlem1  46190  ibliooicc  46215  stoweidlem34  46278  stoweidlem59  46303  etransclem24  46502  caratheodory  46772  ovnhoilem1  46845  hspdifhsp  46860  smfaddlem2  47008  smflimlem1  47015  smflimlem2  47016  smfmullem4  47038  smfsuplem1  47055  fcoreslem4  47312  fcoresf1  47315  fcoresfo  47317  dfnbgrss  48098  dfnbgrss2  48105  isubgrsubgr  48115  rngchomrnghmresALTV  48525  rngcrescrhmALTV  48526  rhmsubcALTVlem1  48527  funcringcsetcALTV2lem9  48544  ssnn0ssfz  48595  isclatd  49228  nelsubclem  49312  setrec2fun  49937  setrec2mpt  49942