inundif

Description: The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
2		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
3	1 2	orbi12i	$⊢ (x \in (A \cap B) \lor x \in (A ∖ B)) \leftrightarrow ((x \in A \land x \in B) \lor (x \in A \land \neg x \in B))$
4		pm4.42	$⊢ x \in A \leftrightarrow ((x \in A \land x \in B) \lor (x \in A \land \neg x \in B))$
5	3 4	bitr4i	$⊢ (x \in (A \cap B) \lor x \in (A ∖ B)) \leftrightarrow x \in A$
6	5	uneqri	$⊢ (A \cap B) \cup (A ∖ B) = A$

Metamath Proof Explorer

Theorem inundif

Proof