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𝒫A

Proof

Step Hyp Ref Expression
1 elssuni xAxA
2 velpw x𝒫AxA
3 1 2 sylibr xAx𝒫A
4 3 ssriv A𝒫A