Theorem axpweq

Description: Two equivalent ways to express the Power Set Axiom. Note that ax-pow is not used by the proof. When ax-pow is assumed and A is a set, both sides of the biconditional hold. In ZF, both sides hold if and only if A is a set (see pwexr ). (Contributed by NM, 22-Jun-2009)

	Ref	Expression
Assertion	axpweq	$$⊢𝒫A\in \mathrm{V}\leftrightarrow \exists x\forall y\left(\forall z\left(z\in y\to z\in A\right)\to y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwidg	$$⊢𝒫A\in \mathrm{V}\to 𝒫A\in 𝒫𝒫A$$
2		pweq	$$⊢x=𝒫A\to 𝒫x=𝒫𝒫A$$
3	2	eleq2d	$$⊢x=𝒫A\to \left(𝒫A\in 𝒫x\leftrightarrow 𝒫A\in 𝒫𝒫A\right)$$
4	3	spcegv	$$⊢𝒫A\in \mathrm{V}\to \left(𝒫A\in 𝒫𝒫A\to \exists x𝒫A\in 𝒫x\right)$$
5	1 4	mpd	$$⊢𝒫A\in \mathrm{V}\to \exists x𝒫A\in 𝒫x$$
6		elex	$$⊢𝒫A\in 𝒫x\to 𝒫A\in \mathrm{V}$$
7	6	exlimiv	$$⊢\exists x𝒫A\in 𝒫x\to 𝒫A\in \mathrm{V}$$
8	5 7	impbii	$$⊢𝒫A\in \mathrm{V}\leftrightarrow \exists x𝒫A\in 𝒫x$$
9		vex	$$⊢x\in \mathrm{V}$$
10	9	elpw2	$$⊢𝒫A\in 𝒫x\leftrightarrow 𝒫A\subseteq x$$
11		pwss	$$⊢𝒫A\subseteq x\leftrightarrow \forall y\left(y\subseteq A\to y\in x\right)$$
12		dfss2	$$⊢y\subseteq A\leftrightarrow \forall z\left(z\in y\to z\in A\right)$$
13	12	imbi1i	$$⊢\left(y\subseteq A\to y\in x\right)\leftrightarrow \left(\forall z\left(z\in y\to z\in A\right)\to y\in x\right)$$
14	13	albii	$$⊢\forall y\left(y\subseteq A\to y\in x\right)\leftrightarrow \forall y\left(\forall z\left(z\in y\to z\in A\right)\to y\in x\right)$$
15	11 14	bitri	$$⊢𝒫A\subseteq x\leftrightarrow \forall y\left(\forall z\left(z\in y\to z\in A\right)\to y\in x\right)$$
16	10 15	bitri	$$⊢𝒫A\in 𝒫x\leftrightarrow \forall y\left(\forall z\left(z\in y\to z\in A\right)\to y\in x\right)$$
17	16	exbii	$$⊢\exists x𝒫A\in 𝒫x\leftrightarrow \exists x\forall y\left(\forall z\left(z\in y\to z\in A\right)\to y\in x\right)$$
18	8 17	bitri	$$⊢𝒫A\in \mathrm{V}\leftrightarrow \exists x\forall y\left(\forall z\left(z\in y\to z\in A\right)\to y\in x\right)$$