Theorem ssin 3719

Description: Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
ssin

Proof of Theorem ssin

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3686	. . . . 5
2	1	imbi2i 312	. . . 4
3	2	albii 1640	. . 3
4		jcab 863	. . . 4
5	4	albii 1640	. . 3
6		19.26 1680	. . 3
7	3, 5, 6	3bitrri 272	. 2
8		dfss2 3492	. . 3
9		dfss2 3492	. . 3
10	8, 9	anbi12i 697	. 2
11		dfss2 3492	. 2
12	7, 10, 11	3bitr4i 277	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  e.wcel 1818  i^icin 3474  C_wss 3475

This theorem is referenced by:  ssini  3720  ssind  3721  uneqin  3748  disjpss  3877  trin  4555  pwin  4789  fin  5770  epfrs  8183  tcmin  8193  resscntz  16369  subgdmdprd  17081  tgval  19456  eltg3i  19462  innei  19626  cnprest2  19791  subislly  19982  lly1stc  19997  xkohaus  20154  xkoinjcn  20188  opnfbas  20343  supfil  20396  rnelfm  20454  tsmsresOLD  20645  tsmsres  20646  restmetu  21090  chabs2  26435  cmbr4i  26519  pjin3i  27113  mdbr2  27215  dmdbr2  27222  dmdbr5  27227  mdslle1i  27236  mdslle2i  27237  mdslj1i  27238  mdslj2i  27239  mdsl2i  27241  mdslmd1lem1  27244  mdslmd1lem2  27245  mdslmd1i  27248  mdslmd3i  27251  hatomistici  27281  chrelat2i  27284  cvexchlem  27287  mdsymlem1  27322  mdsymlem3  27324  mdsymlem6  27327  dmdbr5ati  27341  pnfneige0  27933  ballotlem2  28427  iccllyscon  28695  wfrlem4  29346  frrlem4  29390  heibor1lem  30305  dochexmidlem1  37187  superficl  37752

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