Theorem eqsstrdi 3991

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  eqsstrrdi  3992  eqimssd  4003  dmxpss  6144  dmsnopss  6187  iotassuni  6483  iotassuniOLD  6490  fvmptss  6980  fvmptss2  6994  funressn  7131  riotassuni  7384  ordsuci  7784  frxp  8105  suppssdm  8156  suppun  8163  suppss  8173  suppssov1  8176  suppssov2  8177  suppss2  8179  suppssfv  8181  oawordeulem  8518  omwordri  8536  oewordri  8556  mapssfset  8824  fodomr  9092  fodomfir  9279  fipwuni  9377  fipwss  9380  ordtypelem6  9476  inf3lemd  9580  cantnfle  9624  cantnflem2  9643  ttrclselem1  9678  en2other2  9962  ackbij1lem15  10186  ackbij2lem3  10193  cfub  10202  cflecard  10206  cfle  10207  fin23lem13  10285  fin23lem29  10294  compsscnvlem  10323  itunitc1  10373  fpwwe2lem11  10594  grur1a  10772  uzssz  12814  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  swrdlend  14618  repswswrd  14749  cshimadifsn  14795  xptrrel  14946  relexpnndm  15007  relexpdmd  15010  relexprnd  15014  relexpfldd  15016  rtrclreclem4  15027  limsupgle  15443  isercolllem2  15632  isercolllem3  15633  isercoll  15634  fsumss  15691  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadcl  16432  sadaddlem  16436  sadasslem  16440  sadeq  16442  smupvallem  16453  smucl  16454  prmreclem4  16890  prmreclem5  16891  1arith  16898  vdwmc2  16950  vdwlem13  16964  ramz2  16995  strfvss  17157  ressbasssg  17207  ressbasssOLD  17210  prdsless  17426  sectss  17714  invss  17723  fullfunc  17870  fthfunc  17871  catccatid  18068  resscatc  18071  catcisolem  18072  catciso  18073  yoniso  18246  gsumpropd2lem  18606  cntzrcl  19259  cntzssv  19260  gsumzmhm  19867  ablfaclem3  20019  rnghmresfn  20528  dfrngc2  20537  rnghmsscmap2  20538  rnghmsscmap  20539  funcrngcsetc  20549  rhmresfn  20557  dfringc2  20566  rhmsscmap2  20567  rhmsscmap  20568  rhmsscrnghm  20574  funcringcsetc  20583  rngcrescrhm  20593  rhmsubclem1  20594  rhmsubclem4  20597  lmhmlsp  20956  evpmss  21495  cssss  21594  frlmplusgval  21673  frlmvscafval  21675  uvcresum  21702  resspsrbas  21883  resspsrvsca  21886  subrgpsr  21887  mplsubglem  21908  ressmplbas  21935  subrgmpl  21939  opsrtoslem2  21963  mpfrcl  21992  ressply1bas  22113  ressply1evl  22257  evls1addd  22258  evls1muld  22259  evls1vsca  22260  evls1fvcl  22262  evls1maprhm  22263  scmatlss  22412  cpmatsubgpmat  22607  toponsspwpw  22809  basdif0  22840  ntrss2  22944  ordtbas2  23078  ordtbas  23079  cncls  23161  cmpfi  23295  comppfsc  23419  kgentopon  23425  ptpjpre1  23458  xkoccn  23506  prdstopn  23515  uzfbas  23785  utoptop  24122  utopbas  24123  setsmstopn  24366  restmetu  24458  tngtopn  24538  iccntr  24710  metdstri  24740  pi1xfrcnvlem  24956  cphsubrglem  25077  tcphcph  25137  rrxnm  25291  rrxbasefi  25310  ovolshftlem1  25410  ovolshft  25412  ovolscalem1  25414  ovolscalem2  25415  ovolsca  25416  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem6  25489  itgioo  25717  limcnlp  25779  dvbsss  25803  dvcnvrelem1  25922  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  pserdv  26339  rlimcnp2  26876  fsumharmonic  26922  chpval2  27129  bday0b  27742  madef  27764  madess  27788  oldssmade  27789  n0sbday  28244  bdayn0p1  28258  tglnssp  28479  perpln1  28637  perpln2  28638  uhgrspansubgr  29218  clwwlknclwwlkdifnum  29909  ocsh  31212  shsss  31242  speccl  31828  elnlfn  31857  pj3i  32137  sumdmdlem2  32348  fcoinver  32533  ffsrn  32652  ssnnssfz  32710  pfxrn2  32861  ccatws1f1o  32873  cycpmrn  33100  cycpmconjslem2  33112  fxpss  33123  inftmrel  33134  ressply1mon1p  33537  ressply1invg  33538  evls1subd  33541  algextdeglem7  33713  algextdeglem8  33714  smatrcl  33786  metidss  33881  fsumcvg4  33940  dya2iocuni  34274  carsgcl  34295  breprexplema  34621  bnj1143  34780  bnj1262  34800  bnj517  34875  kur14lem1  35193  cvmliftmolem2  35269  cvmliftlem15  35285  mrsubrn  35500  msubrn  35516  poimirlem30  37644  mblfinlem2  37652  sdclem2  37736  sstotbnd2  37768  isbnd3  37778  lkrlss  39088  pmapssat  39753  diass  41036  diaintclN  41052  dia2dimlem13  41070  dibintclN  41161  lcfrlem25  41561  lcdvbasess  41588  mapdin  41656  mplsubrgcl  42536  diophin  42760  rmxyelqirr  42898  itgocn  43153  oaabsb  43283  oege1  43295  oege2  43296  oacl2g  43319  tfsconcatb0  43333  ofoafg  43343  ofoaf  43344  fpwfvss  43401  relexp0a  43705  frege131d  43753  fsovrfovd  43998  clsk1indlem2  44031  clsk1indlem3  44032  mnuprd  44265  unirestss  45118  founiiun0  45184  fsumsupp0  45576  limsupequzlem  45720  dvnprodlem1  45944  ibliooicc  45969  stoweidlem34  46032  stoweidlem59  46057  etransclem24  46256  caratheodory  46526  ovnhoilem1  46599  hspdifhsp  46614  smfaddlem2  46762  smflimlem1  46769  smflimlem2  46770  smfmullem4  46792  smfsuplem1  46809  fcoreslem4  47067  fcoresf1  47070  fcoresfo  47072  dfnbgrss  47852  dfnbgrss2  47859  isubgrsubgr  47869  rngchomrnghmresALTV  48267  rngcrescrhmALTV  48268  rhmsubcALTVlem1  48269  funcringcsetcALTV2lem9  48286  ssnn0ssfz  48337  isclatd  48971  nelsubclem  49056  setrec2fun  49681  setrec2mpt  49686