Theorem ssin 3720

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 3687	. . . . 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 1620	. . 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 861	. . . 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 1620	. . 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 1657	. . 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 3493	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
9		dfss2 3493	. . 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 3493	. 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 1377   e. wcel 1767   i^i cin 3475   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490

This theorem is referenced by:  ssini  3721  ssind  3722  uneqin  3749  disjpss  3877  trin  4550  pwin  4784  fin  5763  epfrs  8158  tcmin  8168  resscntz  16164  subgdmdprd  16871  tgval  19223  eltg3i  19229  innei  19392  cnprest2  19557  subislly  19748  lly1stc  19763  xkohaus  19889  xkoinjcn  19923  opnfbas  20078  supfil  20131  rnelfm  20189  tsmsresOLD  20380  tsmsres  20381  restmetu  20825  chabs2  26111  cmbr4i  26195  pjin3i  26789  mdbr2  26891  dmdbr2  26898  dmdbr5  26903  mdslle1i  26912  mdslle2i  26913  mdslj1i  26914  mdslj2i  26915  mdsl2i  26917  mdslmd1lem1  26920  mdslmd1lem2  26921  mdslmd1i  26924  mdslmd3i  26927  hatomistici  26957  chrelat2i  26960  cvexchlem  26963  mdsymlem1  26998  mdsymlem3  27000  mdsymlem6  27003  dmdbr5ati  27017  pnfneige0  27569  ballotlem2  28067  iccllyscon  28335  wfrlem4  28923  frrlem4  28967  heibor1lem  29908  limccog  31162  limcresiooub  31184  limcresioolb  31185  fouriersw  31532  dochexmidlem1  36257  superficl  36772