Theorem eqsstrdi 3959

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  eqsstrrdi  3960  eqimssd  3971  dmxpss  6122  dmsnopss  6165  iotassuni  6460  fvmptss  6948  fvmptss2  6962  funressn  7102  riotassuni  7353  ordsuci  7751  frxp  8066  suppssdm  8117  suppun  8124  suppss  8134  suppssov1  8137  suppssov2  8138  suppss2  8140  suppssfv  8142  oawordeulem  8479  omwordri  8497  oewordri  8518  mapssfset  8788  fodomr  9056  fodomfir  9228  fipwuni  9329  fipwss  9332  ordtypelem6  9428  inf3lemd  9539  cantnfle  9583  cantnflem2  9602  ttrclselem1  9637  en2other2  9922  ackbij1lem15  10146  ackbij2lem3  10153  cfub  10162  cflecard  10166  cfle  10167  fin23lem13  10245  fin23lem29  10254  compsscnvlem  10283  itunitc1  10333  fpwwe2lem11  10555  grur1a  10733  uzssz  12800  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  swrdlend  14607  repswswrd  14737  cshimadifsn  14782  xptrrel  14933  relexpnndm  14994  relexpdmd  14997  relexprnd  15001  relexpfldd  15003  rtrclreclem4  15014  limsupgle  15430  isercolllem2  15619  isercolllem3  15620  isercoll  15621  fsumss  15678  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadcl  16422  sadaddlem  16426  sadasslem  16430  sadeq  16432  smupvallem  16443  smucl  16444  prmreclem4  16881  prmreclem5  16882  1arith  16889  vdwmc2  16941  vdwlem13  16955  ramz2  16986  strfvss  17148  ressbasssg  17198  ressbasssOLD  17201  prdsless  17417  sectss  17710  invss  17719  fullfunc  17866  fthfunc  17867  catccatid  18064  resscatc  18067  catcisolem  18068  catciso  18069  yoniso  18242  gsumpropd2lem  18638  cntzrcl  19293  cntzssv  19294  gsumzmhm  19903  ablfaclem3  20055  rnghmresfn  20591  dfrngc2  20600  rnghmsscmap2  20601  rnghmsscmap  20602  funcrngcsetc  20612  rhmresfn  20620  dfringc2  20629  rhmsscmap2  20630  rhmsscmap  20631  rhmsscrnghm  20637  funcringcsetc  20646  rngcrescrhm  20656  rhmsubclem1  20657  rhmsubclem4  20660  lmhmlsp  21039  evpmss  21561  cssss  21660  frlmplusgval  21739  frlmvscafval  21741  uvcresum  21768  resspsrbas  21948  resspsrvsca  21951  subrgpsr  21952  mplsubglem  21973  ressmplbas  22003  subrgmpl  22007  mplsubrgcl  22008  opsrtoslem2  22032  mpfrcl  22061  ressply1bas  22213  ressply1evl  22356  evls1addd  22357  evls1muld  22358  evls1vsca  22359  evls1fvcl  22361  evls1maprhm  22362  scmatlss  22508  cpmatsubgpmat  22703  toponsspwpw  22905  basdif0  22936  ntrss2  23040  ordtbas2  23174  ordtbas  23175  cncls  23257  cmpfi  23391  comppfsc  23515  kgentopon  23521  ptpjpre1  23554  xkoccn  23602  prdstopn  23611  uzfbas  23881  utoptop  24217  utopbas  24218  setsmstopn  24461  restmetu  24553  tngtopn  24633  iccntr  24805  metdstri  24835  pi1xfrcnvlem  25041  cphsubrglem  25162  tcphcph  25222  rrxnm  25376  rrxbasefi  25395  ovolshftlem1  25494  ovolshft  25496  ovolscalem1  25498  ovolscalem2  25499  ovolsca  25500  uniioombllem2  25568  uniioombllem3a  25569  uniioombllem3  25570  uniioombllem4  25571  uniioombllem6  25573  itgioo  25801  limcnlp  25863  dvbsss  25887  dvcnvrelem1  26002  dvfsumle  26006  dvfsumabs  26008  pserdv  26412  rlimcnp2  26948  fsumharmonic  26993  chpval2  27199  bday0b  27823  madef  27846  madess  27876  oldssmade  27877  oldss  27880  n0bday  28362  bdayn0p1  28379  bdaypw2n0bndlem  28473  bdaypw2n0bnd  28474  tglnssp  28638  perpln1  28796  perpln2  28797  uhgrspansubgr  29378  clwwlknclwwlkdifnum  30068  ocsh  31372  shsss  31402  speccl  31988  elnlfn  32017  pj3i  32297  sumdmdlem2  32508  fcoinver  32693  ffsrn  32820  ssnnssfz  32879  pfxrn2  33019  ccatws1f1o  33030  cycpmrn  33224  cycpmconjslem2  33236  fxpss  33247  inftmrel  33261  ressply1mon1p  33651  ressply1invg  33652  evls1subd  33655  esplyind  33759  algextdeglem7  33907  algextdeglem8  33908  smatrcl  33980  metidss  34075  fsumcvg4  34134  dya2iocuni  34467  carsgcl  34488  breprexplema  34814  bnj1143  34972  bnj1262  34992  bnj517  35067  kur14lem1  35434  cvmliftmolem2  35510  cvmliftlem15  35526  mrsubrn  35741  msubrn  35757  dfttc2g  36734  poimirlem30  38017  mblfinlem2  38025  sdclem2  38109  sstotbnd2  38141  isbnd3  38151  lkrlss  39587  pmapssat  40251  diass  41534  diaintclN  41550  dia2dimlem13  41568  dibintclN  41659  lcfrlem25  42059  lcdvbasess  42086  mapdin  42154  diophin  43221  rmxyelqirr  43355  itgocn  43609  oaabsb  43739  oege1  43751  oege2  43752  oacl2g  43775  tfsconcatb0  43789  ofoafg  43799  ofoaf  43800  fpwfvss  43856  relexp0a  44160  frege131d  44208  fsovrfovd  44453  clsk1indlem2  44486  clsk1indlem3  44487  mnuprd  44720  unirestss  45571  founiiun0  45637  fsumsupp0  46023  limsupequzlem  46165  dvnprodlem1  46389  ibliooicc  46414  stoweidlem34  46477  stoweidlem59  46502  etransclem24  46701  caratheodory  46971  ovnhoilem1  47044  hspdifhsp  47059  smfaddlem2  47207  smflimlem1  47214  smflimlem2  47215  smfmullem4  47237  smfsuplem1  47254  fcoreslem4  47529  fcoresf1  47532  fcoresfo  47534  dfnbgrss  48343  dfnbgrss2  48350  isubgrsubgr  48360  rngchomrnghmresALTV  48770  rngcrescrhmALTV  48771  rhmsubcALTVlem1  48772  funcringcsetcALTV2lem9  48789  ssnn0ssfz  48840  isclatd  49473  nelsubclem  49557  setrec2fun  50182  setrec2mpt  50187