This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssin

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)

Ref Expression
Assertion ssin ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ↔ 𝐴 ⊆ ( 𝐵 ∩ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
2 1 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
3 2 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
4 jcab ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) )
5 4 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) )
6 19.26 ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) )
7 3 5 6 3bitrri ⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) )
8 df-ss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
9 df-ss ⊢ ( 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
10 8 9 anbi12i ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) )
11 df-ss ⊢ ( 𝐴 ⊆ ( 𝐵 ∩ 𝐶 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) )
12 7 10 11 3bitr4i ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ↔ 𝐴 ⊆ ( 𝐵 ∩ 𝐶 ) )