Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseqin2 Structured version   Visualization version   Unicode version

Theorem sseqin2 3642
 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
StepHypRef Expression
1 dfss1 3628 1
 Colors of variables: wff setvar class Syntax hints:   wb 189   wceq 1452   cin 3389   wss 3390 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404 This theorem is referenced by:  dfss4  3668  resabs1  5139  rescnvcnv  5305  sspred  5395  predon  6637  frnsuppeq  6945  wfrlem4  7057  fiint  7866  infxpenlem  8462  ackbij1lem2  8669  uzin  11215  iooval2  11694  fzval2  11813  fz1isolem  12665  dfphi2  14801  ressbas  15257  ressress  15265  sylow3lem2  17358  gsumxp  17686  pgpfac1lem5  17790  cmpsub  20492  fbasrn  20977  cmmbl  22566  voliunlem3  22584  0plef  22709  0pledm  22710  itg1ge0  22723  mbfi1fseqlem5  22756  itg2addlem  22795  dvcmulf  22978  efopn  23682  cmcmlem  27325  pjvec  27430  pjocvec  27431  ssmd2  28046  mdslmd4i  28067  chirredlem2  28125  chirredlem3  28126  dmdbr7ati  28158  lmxrge0  28832  orvcelval  29374  dfon2lem4  30503  frrlem4  30588  mblfinlem3  32043  blssp  32149  lcvexchlem1  32671  glbconN  33013  pmapglb2N  33407  pmapglb2xN  33408  2polssN  33551  polatN  33567  osumcllem1N  33592  osumcllem9N  33600  pexmidlem6N  33611  dihmeetlem11N  34956  dochexmidlem6  35104
 Copyright terms: Public domain W3C validator