Theorem undif

Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998)

	Ref	Expression
Assertion	undif	$$⊢A\subseteq B\leftrightarrow A\cup \left(B\setminus A\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		ssequn1	$$⊢A\subseteq B\leftrightarrow A\cup B=B$$
2		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
3	2	eqeq1i	$$⊢A\cup \left(B\setminus A\right)=B\leftrightarrow A\cup B=B$$
4	1 3	bitr4i	$$⊢A\subseteq B\leftrightarrow A\cup \left(B\setminus A\right)=B$$