Theorem axnulALT2

Description: Alternate proof of axnul , proved from propositional calculus, ax-gen , ax-4 , ax-5 , and ax-inf2 . (Contributed by BTernaryTau, 22-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axnulALT2	$$⊢\exists x\forall y\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		exsimpr	$$⊢\exists x\left(x\in z\wedge \forall y\neg y\in x\right)\to \exists x\forall y\neg y\in x$$
2		ax-inf2	$$⊢\exists z\left(\exists x\left(x\in z\wedge \forall y\neg y\in x\right)\wedge \forall x\left(x\in z\to \exists y\left(y\in z\wedge \forall w\left(w\in y\leftrightarrow \left(w\in x\vee w=x\right)\right)\right)\right)\right)$$
3		simpl	$$⊢\left(\exists x\left(x\in z\wedge \forall y\neg y\in x\right)\wedge \forall x\left(x\in z\to \exists y\left(y\in z\wedge \forall w\left(w\in y\leftrightarrow \left(w\in x\vee w=x\right)\right)\right)\right)\right)\to \exists x\left(x\in z\wedge \forall y\neg y\in x\right)$$
4	2 3	eximii	$$⊢\exists z\exists x\left(x\in z\wedge \forall y\neg y\in x\right)$$
5	1 4	exlimiiv	$$⊢\exists x\forall y\neg y\in x$$