Theorem inssdif0

Description: Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014)

	Ref	Expression
Assertion	inssdif0	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
2	1	imbi1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐶 ) )
3		iman	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐶 ) ↔ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) )
4	2 3	bitri	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐶 ) ↔ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) )
5		eldif	⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) )
6	5	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
7		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) )
8		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
9	6 7 8	3bitr4ri	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) )
10	4 9	xchbinx	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐶 ) ↔ ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) )
11	10	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐶 ) ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) )
12		df-ss	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐶 ) )
13		eq0	⊢ ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) )
14	11 12 13	3bitr4i	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ )