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	⊢ 𝒫 ( 𝐴 ∪ 𝐵 ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
2	1	sspwi	⊢ 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 )
3		undif	⊢ ( 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ ( 𝒫 𝐴 ∪ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ) = 𝒫 ( 𝐴 ∪ 𝐵 ) )
4	2 3	mpbi	⊢ ( 𝒫 𝐴 ∪ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ) = 𝒫 ( 𝐴 ∪ 𝐵 )
5		uncom	⊢ ( 𝒫 𝐴 ∪ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 )
6	4 5	eqtr3i	⊢ 𝒫 ( 𝐴 ∪ 𝐵 ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 )