Theorem ssin 4157

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 3897	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
2	1	imbi2i 339	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		jcab 521	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
5	4	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
6		19.26 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	3, 5, 6	3bitrri 301	. 2 ⊢ ((∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)))
8		dfss2 3901	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
9		dfss2 3901	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
10	8, 9	anbi12i 629	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
11		dfss2 3901	. 2 ⊢ (𝐴 ⊆ (𝐵 ∩ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)))
12	7, 10, 11	3bitr4i 306	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   ∈ wcel 2111   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  ssini  4158  ssind  4159  uneqin  4205  disjpss  4368  trin  5146  pwin  5419  fin  6533  wfrlem4  7941  epfrs  9157  tcmin  9167  resscntz  18454  subgdmdprd  19149  tgval  21560  eltg3i  21566  innei  21730  cnprest2  21895  subislly  22086  lly1stc  22101  xkohaus  22258  xkoinjcn  22292  opnfbas  22447  supfil  22500  rnelfm  22558  tsmsres  22749  restmetu  23177  chabs2  29300  cmbr4i  29384  pjin3i  29977  mdbr2  30079  dmdbr2  30086  dmdbr5  30091  mdslle1i  30100  mdslle2i  30101  mdslj1i  30102  mdslj2i  30103  mdsl2i  30105  mdslmd1lem1  30108  mdslmd1lem2  30109  mdslmd1i  30112  mdslmd3i  30115  hatomistici  30145  chrelat2i  30148  cvexchlem  30151  mdsymlem1  30186  mdsymlem3  30188  mdsymlem6  30191  dmdbr5ati  30205  pnfneige0  31304  ballotlem2  31856  iccllysconn  32610  frrlem4  33239  frrlem13  33248  heibor1lem  35247  dochexmidlem1  38756  superficl  40266  k0004lem1  40850