Theorem eqsstrdi 3988

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

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

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 3928

This theorem is referenced by:  eqsstrrdi  3989  eqimssd  4000  dmxpss  6132  dmsnopss  6175  iotassuni  6471  iotassuniOLD  6478  fvmptss  6962  fvmptss2  6976  funressn  7113  riotassuni  7366  ordsuci  7764  frxp  8082  suppssdm  8133  suppun  8140  suppss  8150  suppssov1  8153  suppssov2  8154  suppss2  8156  suppssfv  8158  oawordeulem  8495  omwordri  8513  oewordri  8533  mapssfset  8801  fodomr  9069  fodomfir  9255  fipwuni  9353  fipwss  9356  ordtypelem6  9452  inf3lemd  9556  cantnfle  9600  cantnflem2  9619  ttrclselem1  9654  en2other2  9938  ackbij1lem15  10162  ackbij2lem3  10169  cfub  10178  cflecard  10182  cfle  10183  fin23lem13  10261  fin23lem29  10270  compsscnvlem  10299  itunitc1  10349  fpwwe2lem11  10570  grur1a  10748  uzssz  12790  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  swrdlend  14594  repswswrd  14725  cshimadifsn  14771  xptrrel  14922  relexpnndm  14983  relexpdmd  14986  relexprnd  14990  relexpfldd  14992  rtrclreclem4  15003  limsupgle  15419  isercolllem2  15608  isercolllem3  15609  isercoll  15610  fsumss  15667  sadcaddlem  16403  sadadd2lem  16405  sadadd3  16407  sadcl  16408  sadaddlem  16412  sadasslem  16416  sadeq  16418  smupvallem  16429  smucl  16430  prmreclem4  16866  prmreclem5  16867  1arith  16874  vdwmc2  16926  vdwlem13  16940  ramz2  16971  strfvss  17133  ressbasssg  17183  ressbasssOLD  17186  prdsless  17402  sectss  17694  invss  17703  fullfunc  17850  fthfunc  17851  catccatid  18048  resscatc  18051  catcisolem  18052  catciso  18053  yoniso  18226  gsumpropd2lem  18588  cntzrcl  19241  cntzssv  19242  gsumzmhm  19851  ablfaclem3  20003  rnghmresfn  20539  dfrngc2  20548  rnghmsscmap2  20549  rnghmsscmap  20550  funcrngcsetc  20560  rhmresfn  20568  dfringc2  20577  rhmsscmap2  20578  rhmsscmap  20579  rhmsscrnghm  20585  funcringcsetc  20594  rngcrescrhm  20604  rhmsubclem1  20605  rhmsubclem4  20608  lmhmlsp  20988  evpmss  21528  cssss  21627  frlmplusgval  21706  frlmvscafval  21708  uvcresum  21735  resspsrbas  21916  resspsrvsca  21919  subrgpsr  21920  mplsubglem  21941  ressmplbas  21968  subrgmpl  21972  opsrtoslem2  21996  mpfrcl  22025  ressply1bas  22146  ressply1evl  22290  evls1addd  22291  evls1muld  22292  evls1vsca  22293  evls1fvcl  22295  evls1maprhm  22296  scmatlss  22445  cpmatsubgpmat  22640  toponsspwpw  22842  basdif0  22873  ntrss2  22977  ordtbas2  23111  ordtbas  23112  cncls  23194  cmpfi  23328  comppfsc  23452  kgentopon  23458  ptpjpre1  23491  xkoccn  23539  prdstopn  23548  uzfbas  23818  utoptop  24155  utopbas  24156  setsmstopn  24399  restmetu  24491  tngtopn  24571  iccntr  24743  metdstri  24773  pi1xfrcnvlem  24989  cphsubrglem  25110  tcphcph  25170  rrxnm  25324  rrxbasefi  25343  ovolshftlem1  25443  ovolshft  25445  ovolscalem1  25447  ovolscalem2  25448  ovolsca  25449  uniioombllem2  25517  uniioombllem3a  25518  uniioombllem3  25519  uniioombllem4  25520  uniioombllem6  25522  itgioo  25750  limcnlp  25812  dvbsss  25836  dvcnvrelem1  25955  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  pserdv  26372  rlimcnp2  26909  fsumharmonic  26955  chpval2  27162  bday0b  27779  madef  27801  madess  27825  oldssmade  27826  oldss  27827  n0sbday  28284  bdayn0p1  28298  tglnssp  28532  perpln1  28690  perpln2  28691  uhgrspansubgr  29271  clwwlknclwwlkdifnum  29959  ocsh  31262  shsss  31292  speccl  31878  elnlfn  31907  pj3i  32187  sumdmdlem2  32398  fcoinver  32583  ffsrn  32702  ssnnssfz  32760  pfxrn2  32911  ccatws1f1o  32923  cycpmrn  33115  cycpmconjslem2  33127  fxpss  33138  inftmrel  33149  ressply1mon1p  33530  ressply1invg  33531  evls1subd  33534  algextdeglem7  33706  algextdeglem8  33707  smatrcl  33779  metidss  33874  fsumcvg4  33933  dya2iocuni  34267  carsgcl  34288  breprexplema  34614  bnj1143  34773  bnj1262  34793  bnj517  34868  kur14lem1  35186  cvmliftmolem2  35262  cvmliftlem15  35278  mrsubrn  35493  msubrn  35509  poimirlem30  37637  mblfinlem2  37645  sdclem2  37729  sstotbnd2  37761  isbnd3  37771  lkrlss  39081  pmapssat  39746  diass  41029  diaintclN  41045  dia2dimlem13  41063  dibintclN  41154  lcfrlem25  41554  lcdvbasess  41581  mapdin  41649  mplsubrgcl  42529  diophin  42753  rmxyelqirr  42891  itgocn  43146  oaabsb  43276  oege1  43288  oege2  43289  oacl2g  43312  tfsconcatb0  43326  ofoafg  43336  ofoaf  43337  fpwfvss  43394  relexp0a  43698  frege131d  43746  fsovrfovd  43991  clsk1indlem2  44024  clsk1indlem3  44025  mnuprd  44258  unirestss  45111  founiiun0  45177  fsumsupp0  45569  limsupequzlem  45713  dvnprodlem1  45937  ibliooicc  45962  stoweidlem34  46025  stoweidlem59  46050  etransclem24  46249  caratheodory  46519  ovnhoilem1  46592  hspdifhsp  46607  smfaddlem2  46755  smflimlem1  46762  smflimlem2  46763  smfmullem4  46785  smfsuplem1  46802  fcoreslem4  47060  fcoresf1  47063  fcoresfo  47065  dfnbgrss  47845  dfnbgrss2  47852  isubgrsubgr  47862  rngchomrnghmresALTV  48260  rngcrescrhmALTV  48261  rhmsubcALTVlem1  48262  funcringcsetcALTV2lem9  48279  ssnn0ssfz  48330  isclatd  48964  nelsubclem  49049  setrec2fun  49674  setrec2mpt  49679