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	|- E. x A. y -. y e. x

Proof

Step	Hyp	Ref	Expression
1		exsimpr	|- ( E. x ( x e. z /\ A. y -. y e. x ) -> E. x A. y -. y e. x )
2		ax-inf2	|- E. z ( E. x ( x e. z /\ A. y -. y e. x ) /\ A. x ( x e. z -> E. y ( y e. z /\ A. w ( w e. y <-> ( w e. x \/ w = x ) ) ) ) )
3		simpl	|- ( ( E. x ( x e. z /\ A. y -. y e. x ) /\ A. x ( x e. z -> E. y ( y e. z /\ A. w ( w e. y <-> ( w e. x \/ w = x ) ) ) ) ) -> E. x ( x e. z /\ A. y -. y e. x ) )
4	2 3	eximii	|- E. z E. x ( x e. z /\ A. y -. y e. x )
5	1 4	exlimiiv	|- E. x A. y -. y e. x