Theorem axpowndlem1

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002)

	Ref	Expression
Assertion	axpowndlem1	$$⊢\forall xx=y\to \left(\neg x=y\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm2.24	$$⊢x=y\to \left(\neg x=y\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$
2	1	sps	$$⊢\forall xx=y\to \left(\neg x=y\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$