This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjdif2

Description: The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019)

		Ref	Expression
	Assertion	disjdif2	$⊢ A \cap B = \emptyset \to A ∖ B = A$

Step	Hyp	Ref	Expression
1		difeq2	$⊢ A \cap B = \emptyset \to A ∖ (A \cap B) = A ∖ \emptyset$
2		difin	$⊢ A ∖ (A \cap B) = A ∖ B$
3		dif0	$⊢ A ∖ \emptyset = A$
4	1 2 3	3eqtr3g	$⊢ A \cap B = \emptyset \to A ∖ B = A$