Theorem pwundif

Description: Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007) (Proof shortened by Thierry Arnoux, 20-Dec-2016) Remove use of ax-sep , ax-nul , ax-pr and shorten proof. (Revised by BJ, 14-Apr-2024)

	Ref	Expression
Assertion	pwundif	$$⊢𝒫\left(A\cup B\right)=\left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)\cup 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢A\subseteq A\cup B$$
2	1	sspwi	$$⊢𝒫A\subseteq 𝒫\left(A\cup B\right)$$
3		undif	$$⊢𝒫A\subseteq 𝒫\left(A\cup B\right)\leftrightarrow 𝒫A\cup \left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)=𝒫\left(A\cup B\right)$$
4	2 3	mpbi	$$⊢𝒫A\cup \left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)=𝒫\left(A\cup B\right)$$
5		uncom	$$⊢𝒫A\cup \left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)=\left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)\cup 𝒫A$$
6	4 5	eqtr3i	$$⊢𝒫\left(A\cup B\right)=\left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)\cup 𝒫A$$