Theorem ssin 4138

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 4096	. . . . 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 3901	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
9		df-ss 3901	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
10	8, 9	anbi12i 640	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
11		df-ss 3901	. 2 ⊢ (𝐴 ⊆ (𝐵 ∩ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)))
12	7, 10, 11	3bitr4i 306	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  ssini  4139  ssind  4140  uneqin  4237  disjpss  4417  trin  5227  pwin  5546  fin  6784  frrlem4  8335  frrlem13  8344  epfrs  9759  tcmin  9767  resscntz  19577  subgdmdprd  20280  tgval  23303  eltg3i  23309  innei  23473  cnprest2  23638  subislly  23830  lly1stc  23845  xkohaus  24002  xkoinjcn  24036  opnfbas  24191  supfil  24244  rnelfm  24302  tsmsres  24493  restmetu  24919  chabs2  32149  cmbr4i  32233  pjin3i  32826  mdbr2  32928  dmdbr2  32935  dmdbr5  32940  mdslle1i  32949  mdslle2i  32950  mdslj1i  32951  mdslj2i  32952  mdsl2i  32954  mdslmd1lem1  32957  mdslmd1lem2  32958  mdslmd1i  32961  mdslmd3i  32964  hatomistici  32994  chrelat2i  32997  cvexchlem  33000  mdsymlem1  33035  mdsymlem3  33037  mdsymlem6  33040  dmdbr5ati  33054  pnfneige0  34653  ballotlem2  35191  iccllysconn  36182  heibor1lem  38935  relssinxpdmrn  39473  dochexmidlem1  42709  superficl  44760  k0004lem1  45339  ismnushort  45477