Theorem sseqin2 3716

Description: A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)

Assertion

Ref	Expression
sseqin2

Proof of Theorem sseqin2

Step	Hyp	Ref	Expression
1		dfss1 3702	1

Syntax hints:  <->wb 184  =wceq 1395  i^icin 3474  C_wss 3475

This theorem is referenced by:  dfss4  3731  resabs1  5307  rescnvcnv  5475  frnsuppeq  6930  fiint  7817  infxpenlem  8412  ackbij1lem2  8622  nn0suppOLD  10875  uzin  11142  iooval2  11591  fzval2  11704  fz1isolem  12510  dfphi2  14304  ressbas  14687  ressress  14694  sylow3lem2  16648  gsumxp  17004  gsumxpOLD  17006  pgpfac1lem5  17130  cmpsub  19900  fbasrn  20385  cmmbl  21945  voliunlem3  21962  0plef  22079  0pledm  22080  itg1ge0  22093  mbfi1fseqlem5  22126  itg2addlem  22165  dvcmulf  22348  efopn  23039  cmcmlem  26509  pjvec  26614  pjocvec  26615  ssmd2  27231  mdslmd4i  27252  chirredlem2  27310  chirredlem3  27311  dmdbr7ati  27343  lmxrge0  27934  orvcelval  28407  dfon2lem4  29218  sspred  29252  predon  29273  wfrlem4  29346  frrlem4  29390  mblfinlem3  30053  blssp  30249  fsuppeq  31043  lcvexchlem1  34759  glbconN  35101  pmapglb2N  35495  pmapglb2xN  35496  2polssN  35639  polatN  35655  osumcllem1N  35680  osumcllem9N  35688  pexmidlem6N  35699  dihmeetlem11N  37044  dochexmidlem6  37192

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-nfc 2607  df-v 3111  df-in 3482  df-ss 3489