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	$$⊢𝒫x\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-pw	$$⊢𝒫x=\left\{w|w\subseteq x\right\}$$
2		axpow2	$$⊢\exists y\forall z\left(z\subseteq x\to z\in y\right)$$
3	2	sepexi	$$⊢\exists y\forall z\left(z\in y\leftrightarrow z\subseteq x\right)$$
4		sseq1	$$⊢w=z\to \left(w\subseteq x\leftrightarrow z\subseteq x\right)$$
5	4	eqabbw	$$⊢y=\left\{w|w\subseteq x\right\}\leftrightarrow \forall z\left(z\in y\leftrightarrow z\subseteq x\right)$$
6	5	exbii	$$⊢\exists yy=\left\{w|w\subseteq x\right\}\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow z\subseteq x\right)$$
7	3 6	mpbir	$$⊢\exists yy=\left\{w|w\subseteq x\right\}$$
8	7	issetri	$$⊢\left\{w|w\subseteq x\right\}\in \mathrm{V}$$
9	1 8	eqeltri	$$⊢𝒫x\in \mathrm{V}$$