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

Metamath Proof Explorer

Theorem pwunss

Description: The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of Mendelson p. 235. (Contributed by NM, 23-Nov-2003) Remove use of ax-sep , ax-nul , ax-pr and shorten proof. (Revised by BJ, 13-Apr-2024)

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

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  A C_ ( A u. B )
2 1 sspwi 
 |-  ~P A C_ ~P ( A u. B )
3 ssun2 
 |-  B C_ ( A u. B )
4 3 sspwi 
 |-  ~P B C_ ~P ( A u. B )
5 2 4 unssi 
 |-  ( ~P A u. ~P B ) C_ ~P ( A u. B )