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

Metamath Proof Explorer

Theorem difin0ss

Description: Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994) (Proof shortened by Wolf Lammen, 30-Sep-2014)

Ref Expression
Assertion difin0ss ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) = ∅ → ( 𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eq0 ⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) )
2 iman ⊢ ( ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) ↔ ¬ ( 𝑥 ∈ 𝐶 ∧ ¬ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) )
3 elin ⊢ ( 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) )
4 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
5 4 anbi2ci ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ) )
6 annim ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
7 6 anbi2i ⊢ ( ( 𝑥 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ ¬ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) )
8 3 5 7 3bitri ⊢ ( 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ¬ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) )
9 2 8 xchbinxr ⊢ ( ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) ↔ ¬ 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) )
10 ax-2 ⊢ ( ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐵 ) ) )
11 9 10 sylbir ⊢ ( ¬ 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) → ( ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐵 ) ) )
12 11 al2imi ⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) → ∀ 𝑥 ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐵 ) ) )
13 df-ss ⊢ ( 𝐶 ⊆ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) )
14 df-ss ⊢ ( 𝐶 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐵 ) )
15 12 13 14 3imtr4g ⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) → ( 𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵 ) )
16 1 15 sylbi ⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) = ∅ → ( 𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵 ) )