ssdif0

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

		Ref	Expression
	Assertion	ssdif0	$⊢ A \subseteq B \leftrightarrow A ∖ B = \emptyset$

Step	Hyp	Ref	Expression
1		iman	$⊢ (x \in A \to x \in B) \leftrightarrow \neg (x \in A \land \neg x \in B)$
2		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
3	1 2	xchbinxr	$⊢ (x \in A \to x \in B) \leftrightarrow \neg x \in (A ∖ B)$
4	3	albii	$⊢ \forall x (x \in A \to x \in B) \leftrightarrow \forall x \neg x \in (A ∖ B)$
5		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
6		eq0	$⊢ A ∖ B = \emptyset \leftrightarrow \forall x \neg x \in (A ∖ B)$
7	4 5 6	3bitr4i	$⊢ A \subseteq B \leftrightarrow A ∖ B = \emptyset$

Metamath Proof Explorer