Theorem ssin 4184

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	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))

Proof of Theorem ssin

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3915	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
2	1	imbi2i 339	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		jcab 527	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
5	4	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
6		19.26 1903	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	3, 5, 6	3bitrri 301	. 2 ⊢ ((∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)))
8		df-ss 3916	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
9		df-ss 3916	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
10	8, 9	anbi12i 640	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
11		df-ss 3916	. 2 ⊢ (𝐴 ⊆ (𝐵 ∩ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)))
12	7, 10, 11	3bitr4i 306	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2145   ∩ cin 3898   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  ssini  4185  ssind  4186  uneqin  4235  disjpss  4414  trin  5224  pwin  5542  fin  6754  frrlem4  8291  frrlem13  8300  epfrs  9716  tcmin  9724  resscntz  19527  subgdmdprd  20230  tgval  23253  eltg3i  23259  innei  23423  cnprest2  23588  subislly  23780  lly1stc  23795  xkohaus  23952  xkoinjcn  23986  opnfbas  24141  supfil  24194  rnelfm  24252  tsmsres  24443  restmetu  24869  chabs2  32101  cmbr4i  32185  pjin3i  32778  mdbr2  32880  dmdbr2  32887  dmdbr5  32892  mdslle1i  32901  mdslle2i  32902  mdslj1i  32903  mdslj2i  32904  mdsl2i  32906  mdslmd1lem1  32909  mdslmd1lem2  32910  mdslmd1i  32913  mdslmd3i  32916  hatomistici  32946  chrelat2i  32949  cvexchlem  32952  mdsymlem1  32987  mdsymlem3  32989  mdsymlem6  32992  dmdbr5ati  33006  pnfneige0  34565  ballotlem2  35104  iccllysconn  35984  heibor1lem  38711  relssinxpdmrn  39249  dochexmidlem1  42485  superficl  44526  k0004lem1  45106  ismnushort  45244