Theorem zfpow

Description: Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003)

	Ref	Expression
Assertion	zfpow	$$⊢\exists x\forall y\left(\forall x\left(x\in y\to x\in z\right)\to y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-pow	$$⊢\exists x\forall y\left(\forall w\left(w\in y\to w\in z\right)\to y\in x\right)$$
2		elequ1	$$⊢w=x\to \left(w\in y\leftrightarrow x\in y\right)$$
3		elequ1	$$⊢w=x\to \left(w\in z\leftrightarrow x\in z\right)$$
4	2 3	imbi12d	$$⊢w=x\to \left(\left(w\in y\to w\in z\right)\leftrightarrow \left(x\in y\to x\in z\right)\right)$$
5	4	cbvalvw	$$⊢\forall w\left(w\in y\to w\in z\right)\leftrightarrow \forall x\left(x\in y\to x\in z\right)$$
6	5	imbi1i	$$⊢\left(\forall w\left(w\in y\to w\in z\right)\to y\in x\right)\leftrightarrow \left(\forall x\left(x\in y\to x\in z\right)\to y\in x\right)$$
7	6	albii	$$⊢\forall y\left(\forall w\left(w\in y\to w\in z\right)\to y\in x\right)\leftrightarrow \forall y\left(\forall x\left(x\in y\to x\in z\right)\to y\in x\right)$$
8	7	exbii	$$⊢\exists x\forall y\left(\forall w\left(w\in y\to w\in z\right)\to y\in x\right)\leftrightarrow \exists x\forall y\left(\forall x\left(x\in y\to x\in z\right)\to y\in x\right)$$
9	1 8	mpbi	$$⊢\exists x\forall y\left(\forall x\left(x\in y\to x\in z\right)\to y\in x\right)$$