Theorem syl6eqss 3553

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
syl6eqss.1
syl6eqss.2

Assertion

Ref	Expression
syl6eqss

Proof of Theorem syl6eqss

Step	Hyp	Ref	Expression
1		syl6eqss.1	. 2
2		syl6eqss.2	. . 3
3	2	a1i 11	. 2
4	1, 3	eqsstrd 3537	1

Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475

This theorem is referenced by:  syl6eqssr  3554  dmxpss  5443  dmsnopss  5485  iotassuni  5572  fvmptss  5964  fvmptss2  5975  fimacnv  6019  funressn  6084  riotassuniOLD  6294  frxp  6910  suppssdm  6931  suppun  6939  suppss  6949  suppssov1  6951  suppss2  6953  suppssfv  6955  oawordeulem  7222  omwordri  7240  oewordri  7260  fodomr  7688  fipwuni  7906  fipwss  7909  ordtypelem6  7969  inf3lemd  8065  cantnfle  8111  cantnflem2  8130  cantnfleOLD  8141  en2other2  8408  ackbij1lem15  8635  ackbij2lem3  8642  cfub  8650  cflecard  8654  cfle  8655  fin23lem13  8733  fin23lem29  8742  compsscnvlem  8771  itunitc1  8821  fpwwe2lem12  9040  grur1a  9218  uzssz  11129  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  swrdlend  12656  repswswrd  12756  limsupgle  13300  isercolllem2  13488  isercoll  13490  fsumss  13547  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadcl  14112  sadaddlem  14116  sadasslem  14120  sadeq  14122  smupvallem  14133  smucl  14134  prmreclem4  14437  prmreclem5  14438  1arith  14445  vdwmc2  14497  vdwlem13  14511  ramz2  14542  strfvss  14650  ressbasss  14689  prdsless  14860  sectss  15147  invss  15155  fullfunc  15275  fthfunc  15276  catccatid  15429  resscatc  15432  catcisolem  15433  catciso  15434  yoniso  15554  gsumpropd2lem  15900  cntzrcl  16365  cntzssv  16366  gsumzmhm  16957  ablfaclem3  17138  lmhmlsp  17695  resspsrbas  18070  resspsrvsca  18073  subrgpsr  18074  mplsubglem  18093  mplsubglemOLD  18095  ressmplbas  18118  subrgmpl  18122  mpfrcl  18187  ressply1bas  18270  ply1coeOLD  18338  evpmss  18622  cssss  18716  frlmplusgval  18797  frlmvscafval  18799  uvcresum  18824  scmatlss  19027  cpmatsubgpmat  19221  basdif0  19454  ntrss2  19558  ordtbas2  19692  ordtbas  19693  cncls  19775  cmpfi  19908  comppfsc  20033  kgentopon  20039  ptpjpre1  20072  xkoccn  20120  prdstopn  20129  uzfbas  20399  utoptop  20737  utopbas  20738  setsmstopn  20981  restmetu  21090  tngtopn  21164  iccntr  21326  metdstri  21355  pi1xfrcnvlem  21556  cphsubrglem  21624  tchcph  21680  rrxnm  21823  ovolshftlem1  21920  ovolshft  21922  ovolscalem1  21924  ovolscalem2  21925  ovolsca  21926  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem6  21997  itgioo  22222  limcnlp  22282  dvbsss  22306  dvcnvrelem1  22418  dvfsumle  22422  dvfsumabs  22424  pserdv  22824  rlimcnp2  23296  fsumharmonic  23341  chpval2  23493  tglnssp  23939  perpln1  24087  perpln2  24088  nbgrassvt  24433  clwwlksswrd  24777  subgornss  25308  ocsh  26201  shsss  26231  speccl  26818  elnlfn  26847  pj3i  27127  sumdmdlem2  27338  fcoinver  27460  ffsrn  27552  ssnnssfz  27597  inftmrel  27724  metidss  27870  fsumcvg4  27932  dya2iocuni  28254  kur14lem1  28650  cvmliftmolem2  28727  cvmliftlem15  28743  mrsubrn  28873  msubrn  28889  trpredlem1  29310  wfrlem15  29357  mblfinlem2  30052  sdclem2  30235  sstotbnd2  30270  isbnd3  30280  diophin  30706  itgocn  31113  ibliooicc  31770  stoweidlem34  31816  stoweidlem59  31841  etransclem24  32041  rnghmresfn  32771  rnghmsscmap2  32781  rnghmsscmap  32782  rngchomrnghmresOLD  32804  funcrngcsetc  32806  rhmresfn  32817  dfringc2  32826  rhmsscmap2  32827  rhmsscmap  32828  rhmsscrnghm  32834  funcringcsetc  32843  funcringcsetcOLD2lem9  32852  rngcrescrhm  32893  rhmsubclem1  32894  rhmsubclem4  32897  rngcrescrhmOLD  32912  rhmsubcOLDlem1  32913  ssnn0ssfz  32938  bnj1143  33849  bnj1262  33869  bnj517  33943  lkrlss  34820  pmapssat  35483  diass  36769  diaintclN  36785  dia2dimlem13  36803  dibintclN  36894  lcfrlem25  37294  lcdvbasess  37321  mapdin  37389  xptrrel  37775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489