Theorem ssin 2235

Description: Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.

Assertion

Ref	Expression
ssin	⊢ ((A ⊆ B ⋀ A ⊆ C) ↔ A ⊆ (B ∩ C))

Proof of Theorem ssin

Step	Hyp	Ref	Expression
1		ineq12 2215	. . . . 5 ⊢ (((A ∩ B) = A ⋀ (A ∩ C) = A) → ((A ∩ B) ∩ (A ∩ C)) = (A ∩ A))
2		inindi 2230	. . . . 5 ⊢ (A ∩ (B ∩ C)) = ((A ∩ B) ∩ (A ∩ C))
3	1, 2	syl5eq 1522	. . . 4 ⊢ (((A ∩ B) = A ⋀ (A ∩ C) = A) → (A ∩ (B ∩ C)) = (A ∩ A))
4		inidm 2225	. . . 4 ⊢ (A ∩ A) = A
5	3, 4	syl6eq 1526	. . 3 ⊢ (((A ∩ B) = A ⋀ (A ∩ C) = A) → (A ∩ (B ∩ C)) = A)
6		df-ss 2056	. . . 4 ⊢ (A ⊆ B ↔ (A ∩ B) = A)
7		df-ss 2056	. . . 4 ⊢ (A ⊆ C ↔ (A ∩ C) = A)
8	6, 7	anbi12i 484	. . 3 ⊢ ((A ⊆ B ⋀ A ⊆ C) ↔ ((A ∩ B) = A ⋀ (A ∩ C) = A))
9		df-ss 2056	. . 3 ⊢ (A ⊆ (B ∩ C) ↔ (A ∩ (B ∩ C)) = A)
10	5, 8, 9	3imtr4 219	. 2 ⊢ ((A ⊆ B ⋀ A ⊆ C) → A ⊆ (B ∩ C))
11		inss1 2233	. . . 4 ⊢ (B ∩ C) ⊆ B
12		sstr2 2074	. . . 4 ⊢ (A ⊆ (B ∩ C) → ((B ∩ C) ⊆ B → A ⊆ B))
13	11, 12	mpi 44	. . 3 ⊢ (A ⊆ (B ∩ C) → A ⊆ B)
14		inss2 2234	. . . 4 ⊢ (B ∩ C) ⊆ C
15		sstr2 2074	. . . 4 ⊢ (A ⊆ (B ∩ C) → ((B ∩ C) ⊆ C → A ⊆ C))
16	14, 15	mpi 44	. . 3 ⊢ (A ⊆ (B ∩ C) → A ⊆ C)
17	13, 16	jca 288	. 2 ⊢ (A ⊆ (B ∩ C) → (A ⊆ B ⋀ A ⊆ C))
18	10, 17	impbi 157	1 ⊢ ((A ⊆ B ⋀ A ⊆ C) ↔ A ⊆ (B ∩ C))

Syntax hints:   ↔ wb 146   ⋀ wa 223   = wceq 958   ∩ cin 2049   ⊆ wss 2050

This theorem is referenced by:  ssini 2236  nssinpss 2243  uneqin 2259  disjpss 2323  trin 2695  pwin 2831  fin 3657  zfregs 4657  tgvalt 7615  elcls 7701  innei 7733  chabs2t 9435  cmbr4 9539  pjin3 10117  mdbr2 10218  dmdbr2 10225  dmdbr5 10230  mdslle1 10239  mdslle2 10240  mdslj1 10241  mdslj2 10242  mdsl2 10244  mdsl2b 10245  mdslmd1lem1 10247  mdslmd1lem2 10248  mdslmd1 10251  mdslmd3 10254  hatomistic 10284  chrelat2 10287  cvexchlem 10290  mdsymlem1 10325  mdsymlem3 10327  mdsymlem5 10329  mdsymlem6 10330  dmdbr5at 10344  filintf 10554

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054  df-ss 2056

Copyright terms: Public domain