Metamath Proof Explorer

Theorem pwuni

Description: A class is a subclass of the power class of its union. Exercise 6(b) of Enderton p. 38. (Contributed by NM, 14-Oct-1996)

Ref Expression
Assertion pwuni 
|- A C_ ~P U. A

Proof

Step Hyp Ref Expression
1 elssuni 
 |-  ( x e. A -> x C_ U. A )
2 velpw 
 |-  ( x e. ~P U. A <-> x C_ U. A )
3 1 2 sylibr 
 |-  ( x e. A -> x e. ~P U. A )
4 3 ssriv 
 |-  A C_ ~P U. A