Theorem axprlem1

Description: Lemma for axpr . There exists a set to which all empty sets belong. (Contributed by Rohan Ridenour, 10-Aug-2023) (Revised by BJ, 13-Aug-2023) (Proof shortened by Matthew House, 6-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ax-pow	$$⊢\exists x\forall y\left(\forall z\left(z\in y\to z\in w\right)\to y\in x\right)$$
2		pm2.21	$$⊢\neg z\in y\to \left(z\in y\to z\in w\right)$$
3	2	alimi	$$⊢\forall z\neg z\in y\to \forall z\left(z\in y\to z\in w\right)$$
4	3	imim1i	$$⊢\left(\forall z\left(z\in y\to z\in w\right)\to y\in x\right)\to \left(\forall z\neg z\in y\to y\in x\right)$$
5	4	alimi	$$⊢\forall y\left(\forall z\left(z\in y\to z\in w\right)\to y\in x\right)\to \forall y\left(\forall z\neg z\in y\to y\in x\right)$$
6	1 5	eximii	$$⊢\exists x\forall y\left(\forall z\neg z\in y\to y\in x\right)$$