disj4

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004)

		Ref	Expression
	Assertion	disj4	$⊢ A \cap B = \emptyset \leftrightarrow \neg A ∖ B \subset A$

Step	Hyp	Ref	Expression
1		disj3	$⊢ A \cap B = \emptyset \leftrightarrow A = A ∖ B$
2		eqcom	$⊢ A = A ∖ B \leftrightarrow A ∖ B = A$
3		difss	$⊢ A ∖ B \subseteq A$
4		dfpss2	$⊢ A ∖ B \subset A \leftrightarrow (A ∖ B \subseteq A \land \neg A ∖ B = A)$
5	3 4	mpbiran	$⊢ A ∖ B \subset A \leftrightarrow \neg A ∖ B = A$
6	5	con2bii	$⊢ A ∖ B = A \leftrightarrow \neg A ∖ B \subset A$
7	1 2 6	3bitri	$⊢ A \cap B = \emptyset \leftrightarrow \neg A ∖ B \subset A$

Metamath Proof Explorer