Theorem ssin 3560

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 3527	. . . . 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 1613	. . 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 851	. . . 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 1613	. . 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 3333	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
9		dfss2 3333	. . 3 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
10	8, 9	anbi12i 690	. 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 3333	. 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 1360   e. wcel 1755   i^i cin 3315   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330

This theorem is referenced by:  ssini  3561  ssind  3562  uneqin  3589  disjpss  3717  trin  4383  pwin  4612  fin  5579  epfrs  7939  tcmin  7949  resscntz  15828  subgdmdprd  16504  tgval  18401  eltg3i  18407  innei  18570  cnprest2  18735  subislly  18926  lly1stc  18941  xkohaus  19067  xkoinjcn  19101  opnfbas  19256  supfil  19309  rnelfm  19367  tsmsresOLD  19558  tsmsres  19559  restmetu  20003  chabs2  24742  cmbr4i  24826  pjin3i  25420  mdbr2  25522  dmdbr2  25529  dmdbr5  25534  mdslle1i  25543  mdslle2i  25544  mdslj1i  25545  mdslj2i  25546  mdsl2i  25548  mdslmd1lem1  25551  mdslmd1lem2  25552  mdslmd1i  25555  mdslmd3i  25558  hatomistici  25588  chrelat2i  25591  cvexchlem  25594  mdsymlem1  25629  mdsymlem3  25631  mdsymlem6  25634  dmdbr5ati  25648  pnfneige0  26234  ballotlem2  26718  iccllyscon  26986  wfrlem4  27573  frrlem4  27617  heibor1lem  28549  dochexmidlem1  34675