This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )