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	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) = ∅ → ( 𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵 ) )