Metamath Proof Explorer

Theorem pwundifOLD

Description: Obsolete proof of pwundif as of 26-Dec-2023. (Contributed by NM, 25-Mar-2007) (Proof shortened by Thierry Arnoux, 20-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pwundifOLD 
|- ~P ( A u. B ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A )

Proof

Step Hyp Ref Expression
1 undif1 
 |-  ( ( ~P ( A u. B ) \ ~P A ) u. ~P A ) = ( ~P ( A u. B ) u. ~P A )
2 pwunss 
 |-  ( ~P A u. ~P B ) C_ ~P ( A u. B )
3 unss 
 |-  ( ( ~P A C_ ~P ( A u. B ) /\ ~P B C_ ~P ( A u. B ) ) <-> ( ~P A u. ~P B ) C_ ~P ( A u. B ) )
4 2 3 mpbir 
 |-  ( ~P A C_ ~P ( A u. B ) /\ ~P B C_ ~P ( A u. B ) )
5 4 simpli 
 |-  ~P A C_ ~P ( A u. B )
6 ssequn2 
 |-  ( ~P A C_ ~P ( A u. B ) <-> ( ~P ( A u. B ) u. ~P A ) = ~P ( A u. B ) )
7 5 6 mpbi 
 |-  ( ~P ( A u. B ) u. ~P A ) = ~P ( A u. B )
8 1 7 eqtr2i 
 |-  ~P ( A u. B ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A )