Theorem ssin 3716

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 3683	. . . . 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 1641	. . 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 863	. . . 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 1641	. . 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 1681	. . 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 3488	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
9		dfss2 3488	. . 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 3488	. 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 1393   e. wcel 1819   i^i cin 3470   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485

This theorem is referenced by:  ssini  3717  ssind  3718  uneqin  3756  disjpss  3880  trin  4560  pwin  4793  fin  5771  epfrs  8179  tcmin  8189  resscntz  16495  subgdmdprd  17207  tgval  19582  eltg3i  19588  innei  19752  cnprest2  19917  subislly  20107  lly1stc  20122  xkohaus  20279  xkoinjcn  20313  opnfbas  20468  supfil  20521  rnelfm  20579  tsmsresOLD  20770  tsmsres  20771  restmetu  21215  chabs2  26561  cmbr4i  26645  pjin3i  27239  mdbr2  27341  dmdbr2  27348  dmdbr5  27353  mdslle1i  27362  mdslle2i  27363  mdslj1i  27364  mdslj2i  27365  mdsl2i  27367  mdslmd1lem1  27370  mdslmd1lem2  27371  mdslmd1i  27374  mdslmd3i  27377  hatomistici  27407  chrelat2i  27410  cvexchlem  27413  mdsymlem1  27448  mdsymlem3  27450  mdsymlem6  27453  dmdbr5ati  27467  pnfneige0  28086  ballotlem2  28602  iccllyscon  28870  wfrlem4  29520  frrlem4  29564  heibor1lem  30467  dochexmidlem1  37288  superficl  37853