Theorem undif5

Description: An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024)

	Ref	Expression
Assertion	undif5	$$⊢A\cap B=\varnothing \to \left(A\cup B\right)\setminus B=A$$

Proof

Step	Hyp	Ref	Expression
1		difun2	$$⊢\left(A\cup B\right)\setminus B=A\setminus B$$
2		disjdif2	$$⊢A\cap B=\varnothing \to A\setminus B=A$$
3	1 2	syl5eq	$$⊢A\cap B=\varnothing \to \left(A\cup B\right)\setminus B=A$$