Theorem syl6eqss 3443

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

Syntax hints:  ->wi 4  =wceq 1670  C_wss 3365

This theorem is referenced by:  syl6eqssr  3444  dmxpss  5290  dmsnopss  5331  iotassuni  5417  fvmptss  5798  fvmptss2  5809  fimacnv  5851  funressn  5910  riotassuniOLD  6101  frxp  6688  oawordeulem  6959  omwordri  6977  oewordri  6997  map0e  7214  fodomr  7423  fipwuni  7598  fipwss  7601  ordtypelem6  7659  inf3lemd  7749  cantnfle  7793  cantnflem2  7813  en2other2  8062  ackbij1lem15  8285  ackbij2lem3  8292  cfub  8300  cflecard  8304  cfle  8305  fin23lem13  8383  fin23lem29  8392  compsscnvlem  8421  itunitc1  8471  fpwwe2lem12  8687  grur1a  8865  uzssz  10744  swrdlend  12172  repswswrd  12269  limsupgle  12802  isercolllem2  12990  isercoll  12992  fsumss  13050  sadcaddlem  13500  sadadd2lem  13502  sadadd3  13504  sadcl  13505  sadaddlem  13509  sadasslem  13513  sadeq  13515  smupvallem  13526  smucl  13527  prmreclem4  13827  prmreclem5  13828  1arith  13835  vdwmc2  13887  vdwlem13  13901  ramz2  13932  strfvss  14039  ressbasss  14075  prdsless  14239  sectss  14532  invss  14540  fullfunc  14657  fthfunc  14658  catccatid  14811  resscatc  14814  catcisolem  14815  catciso  14816  yoniso  14936  cntzrcl  15735  cntzssv  15736  ablfaclem3  16260  lmhmlsp  16744  resspsrbas  17103  resspsrvsca  17106  subrgpsr  17107  mplsubglem  17123  ressmplbas  17144  subrgmpl  17148  ressply1bas  17248  cssss  17537  evpmss  17681  frlmplusgval  17719  frlmvscafval  17720  basdif0  18032  ntrss2  18135  ordtbas2  18269  ordtbas  18270  cncls  18352  cmpfi  18485  kgentopon  18585  ptpjpre1  18618  xkoccn  18666  prdstopn  18675  uzfbas  18945  utoptop  19279  utopbas  19280  setsmstopn  19523  restmetu  19632  tngtopn  19706  iccntr  19867  metdstri  19896  pi1xfrcnvlem  20096  cphsubrglem  20155  tchcph  20209  ovolshftlem1  20420  ovolshft  20422  ovolscalem1  20424  ovolscalem2  20425  ovolsca  20426  uniioombllem2  20490  uniioombllem3a  20491  uniioombllem3  20492  uniioombllem4  20493  uniioombllem6  20495  itgioo  20720  limcnlp  20780  dvbsss  20804  dvcnvrelem1  20916  dvfsumle  20920  dvfsumabs  20922  mpfrcl  20954  pserdv  21360  rlimcnp2  21826  fsumharmonic  21871  chpval2  22023  nbgrassvt  22466  subgornss  22915  ocsh  23808  shsss  23838  speccl  24425  elnlfn  24454  pj3i  24734  sumdmdlem2  24945  ffsrn  25159  ssnnssfz  25206  inftmrel  25329  gsumpropd2lem  25401  metidss  25497  fsumcvg4  25559  dya2iocuni  25878  kur14lem1  26240  cvmliftmolem2  26317  cvmliftlem15  26333  trpredlem1  26844  wfrlem15  26891  mblfinlem2  27609  comppfsc  27759  sdclem2  27818  sstotbnd2  27855  isbnd3  27865  diophin  28259  itgocn  28709  stoweidlem34  29008  stoweidlem59  29033  clwwlksswrd  29621  bnj1143  30631  bnj1262  30652  bnj517  30726  lkrlss  31443  pmapssat  32106  diass  33390  diaintclN  33406  dia2dimlem13  33424  dibintclN  33515  lcfrlem25  33915  lcdvbasess  33942  mapdin  34010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470

This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-in 3372  df-ss 3379