Theorem ssdif0

Description: Subclass expressed in terms of difference. Exercise 7 of TakeutiZaring p. 22. (Contributed by NM, 29-Apr-1994)

	Ref	Expression
Assertion	ssdif0	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∖ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		iman	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
2		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
3	1 2	xchbinxr	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
4	3	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
5		df-ss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
6		eq0	⊢ ( ( 𝐴 ∖ 𝐵 ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
7	4 5 6	3bitr4i	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∖ 𝐵 ) = ∅ )