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	|- ~P ( A u. B ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A )

Proof

Step	Hyp	Ref	Expression
1		ssun1	|- A C_ ( A u. B )
2	1	sspwi	|- ~P A C_ ~P ( A u. B )
3		undif	|- ( ~P A C_ ~P ( A u. B ) <-> ( ~P A u. ( ~P ( A u. B ) \ ~P A ) ) = ~P ( A u. B ) )
4	2 3	mpbi	|- ( ~P A u. ( ~P ( A u. B ) \ ~P A ) ) = ~P ( A u. B )
5		uncom	|- ( ~P A u. ( ~P ( A u. B ) \ ~P A ) ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A )
6	4 5	eqtr3i	|- ~P ( A u. B ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A )