dfss6

Description: Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020)

		Ref	Expression
	Assertion	dfss6	$⊢ A \subseteq B \leftrightarrow \neg \exists x (x \in A \land \neg x \in B)$

Step	Hyp	Ref	Expression
1		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
2		notnotb	$⊢ \forall x (x \in A \to x \in B) \leftrightarrow \neg \neg \forall x (x \in A \to x \in B)$
3	1 2	bitri	$⊢ A \subseteq B \leftrightarrow \neg \neg \forall x (x \in A \to x \in B)$
4		exanali	$⊢ \exists x (x \in A \land \neg x \in B) \leftrightarrow \neg \forall x (x \in A \to x \in B)$
5	3 4	xchbinxr	$⊢ A \subseteq B \leftrightarrow \neg \exists x (x \in A \land \neg x \in B)$

Metamath Proof Explorer