Metamath Proof Explorer


Theorem pwexd

Description: Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis pwexd.1 φ A V
Assertion pwexd φ 𝒫 A V

Proof

Step Hyp Ref Expression
1 pwexd.1 φ A V
2 pwexg A V 𝒫 A V
3 1 2 syl φ 𝒫 A V