Metamath Proof Explorer

Theorem pwunssOLD

Description: Obsolete version of pwunss as of 30-Dec-2023. (Contributed by NM, 23-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pwunssOLD 
|- ( ~P A u. ~P B ) C_ ~P ( A u. B )

Proof

Step Hyp Ref Expression
1 ssun 
 |-  ( ( x C_ A \/ x C_ B ) -> x C_ ( A u. B ) )
2 elun 
 |-  ( x e. ( ~P A u. ~P B ) <-> ( x e. ~P A \/ x e. ~P B ) )
3 velpw 
 |-  ( x e. ~P A <-> x C_ A )
4 velpw 
 |-  ( x e. ~P B <-> x C_ B )
5 3 4 orbi12i 
 |-  ( ( x e. ~P A \/ x e. ~P B ) <-> ( x C_ A \/ x C_ B ) )
6 2 5 bitri 
 |-  ( x e. ( ~P A u. ~P B ) <-> ( x C_ A \/ x C_ B ) )
7 velpw 
 |-  ( x e. ~P ( A u. B ) <-> x C_ ( A u. B ) )
8 1 6 7 3imtr4i 
 |-  ( x e. ( ~P A u. ~P B ) -> x e. ~P ( A u. B ) )
9 8 ssriv 
 |-  ( ~P A u. ~P B ) C_ ~P ( A u. B )