Theorem ssin 4205

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 4167	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
2	1	imbi2i 338	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	albii 1814	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		jcab 520	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
5	4	albii 1814	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
6		19.26 1865	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	3, 5, 6	3bitrri 300	. 2 ⊢ ((∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)))
8		dfss2 3953	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
9		dfss2 3953	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
10	8, 9	anbi12i 628	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
11		dfss2 3953	. 2 ⊢ (𝐴 ⊆ (𝐵 ∩ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)))
12	7, 10, 11	3bitr4i 305	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1529   ∈ wcel 2108   ∩ cin 3933   ⊆ wss 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-in 3941  df-ss 3950

This theorem is referenced by:  ssini  4206  ssind  4207  uneqin  4253  disjpss  4408  trin  5173  pwin  5445  fin  6552  wfrlem4  7950  epfrs  9165  tcmin  9175  resscntz  18454  subgdmdprd  19148  tgval  21555  eltg3i  21561  innei  21725  cnprest2  21890  subislly  22081  lly1stc  22096  xkohaus  22253  xkoinjcn  22287  opnfbas  22442  supfil  22495  rnelfm  22553  tsmsres  22744  restmetu  23172  chabs2  29286  cmbr4i  29370  pjin3i  29963  mdbr2  30065  dmdbr2  30072  dmdbr5  30077  mdslle1i  30086  mdslle2i  30087  mdslj1i  30088  mdslj2i  30089  mdsl2i  30091  mdslmd1lem1  30094  mdslmd1lem2  30095  mdslmd1i  30098  mdslmd3i  30101  hatomistici  30131  chrelat2i  30134  cvexchlem  30137  mdsymlem1  30172  mdsymlem3  30174  mdsymlem6  30177  dmdbr5ati  30191  pnfneige0  31187  ballotlem2  31739  iccllysconn  32490  frrlem4  33119  frrlem13  33128  heibor1lem  35079  dochexmidlem1  38588  superficl  39917  k0004lem1  40488