Theorem syl6eqss 3387

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 3371	1

Syntax hints:  ->wi 4  =wceq 1654  C_wss 3309

This theorem is referenced by:  syl6eqssr  3388  dmxpss  5344  dmsnopss  5388  iotassuni  5480  fvmptss  5861  fvmptss2  5872  fimacnv  5910  funressn  5967  frxp  6506  riotassuni  6637  oawordeulem  6846  omwordri  6864  oewordri  6884  map0e  7100  fodomr  7307  fipwuni  7480  fipwss  7483  ordtypelem6  7541  inf3lemd  7631  cantnfle  7675  cantnflem2  7695  ackbij1lem15  8165  ackbij2lem3  8172  cfub  8180  cflecard  8184  cfle  8185  fin23lem13  8263  fin23lem29  8272  compsscnvlem  8301  itunitc1  8351  fpwwe2lem12  8567  grur1a  8745  uzssz  10556  limsupgle  12322  isercolllem2  12510  isercoll  12512  fsumss  12570  sadcaddlem  13020  sadadd2lem  13022  sadadd3  13024  sadcl  13025  sadaddlem  13029  sadasslem  13033  sadeq  13035  smupvallem  13046  smucl  13047  prmreclem4  13338  prmreclem5  13339  1arith  13346  vdwmc2  13398  vdwlem13  13412  ramz2  13443  strfvss  13538  ressbasss  13572  prdsless  13736  sectss  14029  invss  14037  fullfunc  14154  fthfunc  14155  catccatid  14308  resscatc  14311  catcisolem  14312  catciso  14313  yoniso  14433  cntzrcl  15177  cntzssv  15178  ablfaclem3  15696  lmhmlsp  16176  resspsrbas  16529  resspsrvsca  16532  subrgpsr  16533  mplsubglem  16549  ressmplbas  16570  subrgmpl  16574  ressply1bas  16674  cssss  16963  basdif0  17069  ntrss2  17172  ordtbas2  17306  ordtbas  17307  cncls  17389  cmpfi  17522  kgentopon  17621  ptpjpre1  17654  xkoccn  17702  prdstopn  17711  uzfbas  17981  utoptop  18315  utopbas  18316  setsmstopn  18559  restmetu  18668  tngtopn  18742  iccntr  18903  metdstri  18932  pi1xfrcnvlem  19132  cphsubrglem  19191  tchcph  19245  ovolshftlem1  19456  ovolshft  19458  ovolscalem1  19460  ovolscalem2  19461  ovolsca  19462  uniioombllem2  19526  uniioombllem3a  19527  uniioombllem3  19528  uniioombllem4  19529  uniioombllem6  19531  itgioo  19756  limcnlp  19816  dvbsss  19840  dvcnvrelem1  19952  dvfsumle  19956  dvfsumabs  19958  mpfrcl  19990  pserdv  20396  rlimcnp2  20856  fsumharmonic  20901  chpval2  21053  nbgrassvt  21496  subgornss  21945  ocsh  22836  shsss  22866  speccl  23453  elnlfn  23482  pj3i  23762  sumdmdlem2  23973  ssnnssfz  24197  gsumpropd2lem  24269  inftmrel  24299  metidss  24335  dya2iocuni  24682  ffsrn  24726  fsumcvg4  24739  kur14lem1  24996  cvmliftmolem2  25073  cvmliftlem15  25089  trpredlem1  25609  wfrlem15  25656  mblfinlem2  26353  comppfsc  26498  sdclem2  26557  sstotbnd2  26594  isbnd3  26604  diophin  27012  frlmplusgval  27385  frlmvscafval  27386  itgocn  27525  en2other2  27538  stoweidlem34  27937  stoweidlem59  27962  swrdltnd  28379  bnj1143  29402  bnj1262  29423  bnj517  29497  lkrlss  30133  pmapssat  30796  diass  32080  diaintclN  32096  dia2dimlem13  32114  dibintclN  32205  lcfrlem25  32605  lcdvbasess  32632  mapdin  32700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424

This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3316  df-ss 3323