Metamath Proof Explorer


Theorem nfpw

Description: Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypothesis nfpw.1 _xA
Assertion nfpw _x𝒫A

Proof

Step Hyp Ref Expression
1 nfpw.1 _xA
2 df-pw 𝒫A=y|yA
3 nfcv _xy
4 3 1 nfss xyA
5 4 nfab _xy|yA
6 2 5 nfcxfr _x𝒫A