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	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfpw	$$⊢\underset{\_}{Ⅎ}x𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		nfpw.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-pw	$$⊢𝒫A=\left\{y|y\subseteq A\right\}$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
4	3 1	nfss	$$⊢Ⅎxy\subseteq A$$
5	4	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{y|y\subseteq A\right\}$$
6	2 5	nfcxfr	$$⊢\underset{\_}{Ⅎ}x𝒫A$$