Theorem eqsstrdi 3974

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  eqsstrrdi  3975  eqimssd  3986  dmxpss  6118  dmsnopss  6161  iotassuni  6456  fvmptss  6941  fvmptss2  6955  funressn  7092  riotassuni  7343  ordsuci  7741  frxp  8056  suppssdm  8107  suppun  8114  suppss  8124  suppssov1  8127  suppssov2  8128  suppss2  8130  suppssfv  8132  oawordeulem  8469  omwordri  8487  oewordri  8507  mapssfset  8775  fodomr  9041  fodomfir  9212  fipwuni  9310  fipwss  9313  ordtypelem6  9409  inf3lemd  9517  cantnfle  9561  cantnflem2  9580  ttrclselem1  9615  en2other2  9900  ackbij1lem15  10124  ackbij2lem3  10131  cfub  10140  cflecard  10144  cfle  10145  fin23lem13  10223  fin23lem29  10232  compsscnvlem  10261  itunitc1  10311  fpwwe2lem11  10532  grur1a  10710  uzssz  12753  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  swrdlend  14561  repswswrd  14691  cshimadifsn  14736  xptrrel  14887  relexpnndm  14948  relexpdmd  14951  relexprnd  14955  relexpfldd  14957  rtrclreclem4  14968  limsupgle  15384  isercolllem2  15573  isercolllem3  15574  isercoll  15575  fsumss  15632  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadcl  16373  sadaddlem  16377  sadasslem  16381  sadeq  16383  smupvallem  16394  smucl  16395  prmreclem4  16831  prmreclem5  16832  1arith  16839  vdwmc2  16891  vdwlem13  16905  ramz2  16936  strfvss  17098  ressbasssg  17148  ressbasssOLD  17151  prdsless  17367  sectss  17659  invss  17668  fullfunc  17815  fthfunc  17816  catccatid  18013  resscatc  18016  catcisolem  18017  catciso  18018  yoniso  18191  gsumpropd2lem  18587  cntzrcl  19239  cntzssv  19240  gsumzmhm  19849  ablfaclem3  20001  rnghmresfn  20534  dfrngc2  20543  rnghmsscmap2  20544  rnghmsscmap  20545  funcrngcsetc  20555  rhmresfn  20563  dfringc2  20572  rhmsscmap2  20573  rhmsscmap  20574  rhmsscrnghm  20580  funcringcsetc  20589  rngcrescrhm  20599  rhmsubclem1  20600  rhmsubclem4  20603  lmhmlsp  20983  evpmss  21523  cssss  21622  frlmplusgval  21701  frlmvscafval  21703  uvcresum  21730  resspsrbas  21911  resspsrvsca  21914  subrgpsr  21915  mplsubglem  21936  ressmplbas  21963  subrgmpl  21967  opsrtoslem2  21991  mpfrcl  22020  ressply1bas  22141  ressply1evl  22285  evls1addd  22286  evls1muld  22287  evls1vsca  22288  evls1fvcl  22290  evls1maprhm  22291  scmatlss  22440  cpmatsubgpmat  22635  toponsspwpw  22837  basdif0  22868  ntrss2  22972  ordtbas2  23106  ordtbas  23107  cncls  23189  cmpfi  23323  comppfsc  23447  kgentopon  23453  ptpjpre1  23486  xkoccn  23534  prdstopn  23543  uzfbas  23813  utoptop  24149  utopbas  24150  setsmstopn  24393  restmetu  24485  tngtopn  24565  iccntr  24737  metdstri  24767  pi1xfrcnvlem  24983  cphsubrglem  25104  tcphcph  25164  rrxnm  25318  rrxbasefi  25337  ovolshftlem1  25437  ovolshft  25439  ovolscalem1  25441  ovolscalem2  25442  ovolsca  25443  uniioombllem2  25511  uniioombllem3a  25512  uniioombllem3  25513  uniioombllem4  25514  uniioombllem6  25516  itgioo  25744  limcnlp  25806  dvbsss  25830  dvcnvrelem1  25949  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  pserdv  26366  rlimcnp2  26903  fsumharmonic  26949  chpval2  27156  bday0b  27774  madef  27797  madess  27821  oldssmade  27822  oldss  27823  n0sbday  28280  bdayn0p1  28294  tglnssp  28530  perpln1  28688  perpln2  28689  uhgrspansubgr  29269  clwwlknclwwlkdifnum  29960  ocsh  31263  shsss  31293  speccl  31879  elnlfn  31908  pj3i  32188  sumdmdlem2  32399  fcoinver  32584  ffsrn  32711  ssnnssfz  32770  pfxrn2  32921  ccatws1f1o  32932  cycpmrn  33112  cycpmconjslem2  33124  fxpss  33135  inftmrel  33149  ressply1mon1p  33531  ressply1invg  33532  evls1subd  33535  algextdeglem7  33736  algextdeglem8  33737  smatrcl  33809  metidss  33904  fsumcvg4  33963  dya2iocuni  34296  carsgcl  34317  breprexplema  34643  bnj1143  34802  bnj1262  34822  bnj517  34897  kur14lem1  35250  cvmliftmolem2  35326  cvmliftlem15  35342  mrsubrn  35557  msubrn  35573  poimirlem30  37698  mblfinlem2  37706  sdclem2  37790  sstotbnd2  37822  isbnd3  37832  lkrlss  39142  pmapssat  39806  diass  41089  diaintclN  41105  dia2dimlem13  41123  dibintclN  41214  lcfrlem25  41614  lcdvbasess  41641  mapdin  41709  mplsubrgcl  42589  diophin  42813  rmxyelqirr  42951  itgocn  43205  oaabsb  43335  oege1  43347  oege2  43348  oacl2g  43371  tfsconcatb0  43385  ofoafg  43395  ofoaf  43396  fpwfvss  43453  relexp0a  43757  frege131d  43805  fsovrfovd  44050  clsk1indlem2  44083  clsk1indlem3  44084  mnuprd  44317  unirestss  45169  founiiun0  45235  fsumsupp0  45626  limsupequzlem  45768  dvnprodlem1  45992  ibliooicc  46017  stoweidlem34  46080  stoweidlem59  46105  etransclem24  46304  caratheodory  46574  ovnhoilem1  46647  hspdifhsp  46662  smfaddlem2  46810  smflimlem1  46817  smflimlem2  46818  smfmullem4  46840  smfsuplem1  46857  fcoreslem4  47105  fcoresf1  47108  fcoresfo  47110  dfnbgrss  47891  dfnbgrss2  47898  isubgrsubgr  47908  rngchomrnghmresALTV  48318  rngcrescrhmALTV  48319  rhmsubcALTVlem1  48320  funcringcsetcALTV2lem9  48337  ssnn0ssfz  48388  isclatd  49022  nelsubclem  49107  setrec2fun  49732  setrec2mpt  49737