Metamath Proof Explorer


Theorem velpw

Description: Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion velpw x𝒫AxA

Proof

Step Hyp Ref Expression
1 vex xV
2 1 elpw x𝒫AxA