Theorem vpwex

Description: Power set axiom: the powerclass of a set is a set. Axiom 4 of TakeutiZaring p. 17. (Contributed by NM, 30-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011) Revised to prove pwexg from vpwex . (Revised by BJ, 10-Aug-2022)

	Ref	Expression
Assertion	vpwex	|- ~P x e. _V

Proof

Step	Hyp	Ref	Expression
1		df-pw	|- ~P x = { y | y C_ x }
2		axpow2	|- E. z A. y ( y C_ x -> y e. z )
3	2	bm1.3ii	|- E. z A. y ( y e. z <-> y C_ x )
4		abeq2	|- ( z = { y | y C_ x } <-> A. y ( y e. z <-> y C_ x ) )
5	4	exbii	|- ( E. z z = { y | y C_ x } <-> E. z A. y ( y e. z <-> y C_ x ) )
6	3 5	mpbir	|- E. z z = { y | y C_ x }
7	6	issetri	|- { y | y C_ x } e. _V
8	1 7	eqeltri	|- ~P x e. _V