Theorem ssin 3577

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	|- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )

Proof of Theorem ssin

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3544	. . . . 5 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
2	1	imbi2i 312	. . . 4 |- ( ( x e. A -> x e. ( B i^i C ) ) <-> ( x e. A -> ( x e. B /\ x e. C ) ) )
3	2	albii 1610	. . 3 |- ( A. x ( x e. A -> x e. ( B i^i C ) ) <-> A. x ( x e. A -> ( x e. B /\ x e. C ) ) )
4		jcab 858	. . . 4 |- ( ( x e. A -> ( x e. B /\ x e. C ) ) <-> ( ( x e. A -> x e. B ) /\ ( x e. A -> x e. C ) ) )
5	4	albii 1610	. . 3 |- ( A. x ( x e. A -> ( x e. B /\ x e. C ) ) <-> A. x ( ( x e. A -> x e. B ) /\ ( x e. A -> x e. C ) ) )
6		19.26 1647	. . 3 |- ( A. x ( ( x e. A -> x e. B ) /\ ( x e. A -> x e. C ) ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. A -> x e. C ) ) )
7	3, 5, 6	3bitrri 272	. 2 |- ( ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. A -> x e. C ) ) <-> A. x ( x e. A -> x e. ( B i^i C ) ) )
8		dfss2 3350	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
9		dfss2 3350	. . 3 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
10	8, 9	anbi12i 697	. 2 |- ( ( A C_ B /\ A C_ C ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. A -> x e. C ) ) )
11		dfss2 3350	. 2 |- ( A C_ ( B i^i C ) <-> A. x ( x e. A -> x e. ( B i^i C ) ) )
12	7, 10, 11	3bitr4i 277	1 |- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1367   e. wcel 1756   i^i cin 3332   C_ wss 3333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-ss 3347

This theorem is referenced by:  ssini  3578  ssind  3579  uneqin  3606  disjpss  3734  trin  4400  pwin  4630  fin  5596  epfrs  7956  tcmin  7966  resscntz  15854  subgdmdprd  16536  tgval  18565  eltg3i  18571  innei  18734  cnprest2  18899  subislly  19090  lly1stc  19105  xkohaus  19231  xkoinjcn  19265  opnfbas  19420  supfil  19473  rnelfm  19531  tsmsresOLD  19722  tsmsres  19723  restmetu  20167  chabs2  24925  cmbr4i  25009  pjin3i  25603  mdbr2  25705  dmdbr2  25712  dmdbr5  25717  mdslle1i  25726  mdslle2i  25727  mdslj1i  25728  mdslj2i  25729  mdsl2i  25731  mdslmd1lem1  25734  mdslmd1lem2  25735  mdslmd1i  25738  mdslmd3i  25741  hatomistici  25771  chrelat2i  25774  cvexchlem  25777  mdsymlem1  25812  mdsymlem3  25814  mdsymlem6  25817  dmdbr5ati  25831  pnfneige0  26386  ballotlem2  26876  iccllyscon  27144  wfrlem4  27732  frrlem4  27776  heibor1lem  28713  dochexmidlem1  35110