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\{y|y\subseteq x\right\}$$
2		axpow2	$$⊢\exists z\forall y\left(y\subseteq x\to y\in z\right)$$
3	2	bm1.3ii	$$⊢\exists z\forall y\left(y\in z\leftrightarrow y\subseteq x\right)$$
4		abeq2	$$⊢z=\left\{y|y\subseteq x\right\}\leftrightarrow \forall y\left(y\in z\leftrightarrow y\subseteq x\right)$$
5	4	exbii	$$⊢\exists zz=\left\{y|y\subseteq x\right\}\leftrightarrow \exists z\forall y\left(y\in z\leftrightarrow y\subseteq x\right)$$
6	3 5	mpbir	$$⊢\exists zz=\left\{y|y\subseteq x\right\}$$
7	6	issetri	$$⊢\left\{y|y\subseteq x\right\}\in \mathrm{V}$$
8	1 7	eqeltri	$$⊢𝒫x\in \mathrm{V}$$