Theorem axnulALT2

Description: Alternate proof of axnul , proved from propositional calculus, ax-gen , ax-4 , ax-6 , and ax-rep . (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by BTernaryTau, 27-Mar-2026)

	Ref	Expression
Assertion	axnulALT2	|- E. x A. y -. y e. x

Proof

Step	Hyp	Ref	Expression
1		ax-rep	|- ( A. w E. x A. y ( A. x F. -> y = x ) -> E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
2		fal	|- -. F.
3	2	spfalw	|- ( A. x F. -> F. )
4	2 3	mto	|- -. A. x F.
5	4	pm2.21i	|- ( A. x F. -> y = x )
6	5	ax-gen	|- A. y ( A. x F. -> y = x )
7	6	exgen	|- E. x A. y ( A. x F. -> y = x )
8	1 7	mpg	|- E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) )
9	4	intnan	|- -. ( w e. z /\ A. x F. )
10	9	nex	|- -. E. w ( w e. z /\ A. x F. )
11	10	nbn	|- ( -. y e. x <-> ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
12	11	albii	|- ( A. y -. y e. x <-> A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
13	12	exbii	|- ( E. x A. y -. y e. x <-> E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
14	8 13	mpbir	|- E. x A. y -. y e. x