Metamath Proof Explorer


Theorem pwex

Description: Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis pwex.1 A V
Assertion pwex 𝒫 A V

Proof

Step Hyp Ref Expression
1 pwex.1 A V
2 pwexg A V 𝒫 A V
3 1 2 ax-mp 𝒫 A V