Theorem syl6eqss 3431

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

Syntax hints:  ->wi 4  =wceq 1662  C_wss 3353

This theorem is referenced by:  syl6eqssr  3432  dmxpss  5269  dmsnopss  5310  iotassuni  5396  fvmptss  5774  fvmptss2  5785  fimacnv  5824  funressn  5881  riotassuniOLD  6065  frxp  6639  oawordeulem  6909  omwordri  6927  oewordri  6947  map0e  7163  fodomr  7370  fipwuni  7543  fipwss  7546  ordtypelem6  7604  inf3lemd  7694  cantnfle  7738  cantnflem2  7758  ackbij1lem15  8228  ackbij2lem3  8235  cfub  8243  cflecard  8247  cfle  8248  fin23lem13  8326  fin23lem29  8335  compsscnvlem  8364  itunitc1  8414  fpwwe2lem12  8630  grur1a  8808  uzssz  10687  swrdlend  12112  repswswrd  12208  limsupgle  12741  isercolllem2  12929  isercoll  12931  fsumss  12989  sadcaddlem  13439  sadadd2lem  13441  sadadd3  13443  sadcl  13444  sadaddlem  13448  sadasslem  13452  sadeq  13454  smupvallem  13465  smucl  13466  prmreclem4  13766  prmreclem5  13767  1arith  13774  vdwmc2  13826  vdwlem13  13840  ramz2  13871  strfvss  13978  ressbasss  14012  prdsless  14176  sectss  14469  invss  14477  fullfunc  14594  fthfunc  14595  catccatid  14748  resscatc  14751  catcisolem  14752  catciso  14753  yoniso  14873  cntzrcl  15629  cntzssv  15630  ablfaclem3  16148  lmhmlsp  16628  resspsrbas  16981  resspsrvsca  16984  subrgpsr  16985  mplsubglem  17001  ressmplbas  17022  subrgmpl  17026  ressply1bas  17126  cssss  17415  basdif0  17521  ntrss2  17624  ordtbas2  17758  ordtbas  17759  cncls  17841  cmpfi  17974  kgentopon  18074  ptpjpre1  18107  xkoccn  18155  prdstopn  18164  uzfbas  18434  utoptop  18768  utopbas  18769  setsmstopn  19012  restmetu  19121  tngtopn  19195  iccntr  19356  metdstri  19385  pi1xfrcnvlem  19585  cphsubrglem  19644  tchcph  19698  ovolshftlem1  19909  ovolshft  19911  ovolscalem1  19913  ovolscalem2  19914  ovolsca  19915  uniioombllem2  19979  uniioombllem3a  19980  uniioombllem3  19981  uniioombllem4  19982  uniioombllem6  19984  itgioo  20209  limcnlp  20269  dvbsss  20293  dvcnvrelem1  20405  dvfsumle  20409  dvfsumabs  20411  mpfrcl  20443  pserdv  20849  rlimcnp2  21314  fsumharmonic  21359  chpval2  21511  nbgrassvt  21954  subgornss  22403  ocsh  23296  shsss  23326  speccl  23913  elnlfn  23942  pj3i  24222  sumdmdlem2  24433  ffsrn  24650  ssnnssfz  24697  inftmrel  24820  gsumpropd2lem  24892  metidss  24988  fsumcvg4  25050  dya2iocuni  25369  kur14lem1  25731  cvmliftmolem2  25808  cvmliftlem15  25824  trpredlem1  26335  wfrlem15  26382  mblfinlem2  27100  comppfsc  27250  sdclem2  27309  sstotbnd2  27346  isbnd3  27356  diophin  27762  frlmplusgval  28135  frlmvscafval  28136  itgocn  28275  en2other2  28288  stoweidlem34  28683  stoweidlem59  28708  clwwlksswrd  29299  bnj1143  30354  bnj1262  30375  bnj517  30449  lkrlss  31166  pmapssat  31829  diass  33113  diaintclN  33129  dia2dimlem13  33147  dibintclN  33238  lcfrlem25  33638  lcdvbasess  33665  mapdin  33733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462

This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-in 3360  df-ss 3367