Theorem ssin 3666

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 3629	. . . . 5 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
2	1	imbi2i 318	. . . 4 |- ( ( x e. A -> x e. ( B i^i C ) ) <-> ( x e. A -> ( x e. B /\ x e. C ) ) )
3	2	albii 1702	. . 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 879	. . . 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 1702	. . 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 1743	. . 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 280	. 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 3433	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
9		dfss2 3433	. . 3 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
10	8, 9	anbi12i 708	. 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 3433	. 2 |- ( A C_ ( B i^i C ) <-> A. x ( x e. A -> x e. ( B i^i C ) ) )
12	7, 10, 11	3bitr4i 285	1 |- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   A.wal 1453   e. wcel 1898   i^i cin 3415   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430

This theorem is referenced by:  ssini  3667  ssind  3668  uneqin  3706  disjpss  3827  trin  4521  pwin  4757  fin  5786  wfrlem4  7065  epfrs  8241  tcmin  8251  resscntz  17034  subgdmdprd  17716  tgval  20019  eltg3i  20025  innei  20190  cnprest2  20355  subislly  20545  lly1stc  20560  xkohaus  20717  xkoinjcn  20751  opnfbas  20906  supfil  20959  rnelfm  21017  tsmsres  21207  restmetu  21634  chabs2  27219  cmbr4i  27303  pjin3i  27896  mdbr2  27998  dmdbr2  28005  dmdbr5  28010  mdslle1i  28019  mdslle2i  28020  mdslj1i  28021  mdslj2i  28022  mdsl2i  28024  mdslmd1lem1  28027  mdslmd1lem2  28028  mdslmd1i  28031  mdslmd3i  28034  hatomistici  28064  chrelat2i  28067  cvexchlem  28070  mdsymlem1  28105  mdsymlem3  28107  mdsymlem6  28110  dmdbr5ati  28124  pnfneige0  28806  ballotlem2  29370  iccllyscon  30022  frrlem4  30566  heibor1lem  32186  dochexmidlem1  35073  superficl  36216