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	|- F/_ x A
Assertion	nfpw	|- F/_ x ~P A

Proof

Step	Hyp	Ref	Expression
1		nfpw.1	|- F/_ x A
2		df-pw	|- ~P A = { y | y C_ A }
3		nfcv	|- F/_ x y
4	3 1	nfss	|- F/ x y C_ A
5	4	nfab	|- F/_ x { y | y C_ A }
6	2 5	nfcxfr	|- F/_ x ~P A