Theorem axnultcoreg

Description: Derivation of ax-nul from ax-tco and ax-reg . Use ax-nul instead. (Contributed by Matthew House, 7-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		elequ1	|- ( x = z -> ( x e. w <-> z e. w ) )
2	1	biimprd	|- ( x = z -> ( z e. w -> x e. w ) )
3	2	spimevw	|- ( z e. w -> E. x x e. w )
4		ax-reg	|- ( E. x x e. w -> E. x ( x e. w /\ A. y ( y e. x -> -. y e. w ) ) )
5	3 4	syl	|- ( z e. w -> E. x ( x e. w /\ A. y ( y e. x -> -. y e. w ) ) )
6		pm2.65	|- ( ( y e. x -> y e. w ) -> ( ( y e. x -> -. y e. w ) -> -. y e. x ) )
7	6	al2imi	|- ( A. y ( y e. x -> y e. w ) -> ( A. y ( y e. x -> -. y e. w ) -> A. y -. y e. x ) )
8	7	imim2i	|- ( ( x e. w -> A. y ( y e. x -> y e. w ) ) -> ( x e. w -> ( A. y ( y e. x -> -. y e. w ) -> A. y -. y e. x ) ) )
9	8	impd	|- ( ( x e. w -> A. y ( y e. x -> y e. w ) ) -> ( ( x e. w /\ A. y ( y e. x -> -. y e. w ) ) -> A. y -. y e. x ) )
10	9	aleximi	|- ( A. x ( x e. w -> A. y ( y e. x -> y e. w ) ) -> ( E. x ( x e. w /\ A. y ( y e. x -> -. y e. w ) ) -> E. x A. y -. y e. x ) )
11	5 10	mpan9	|- ( ( z e. w /\ A. x ( x e. w -> A. y ( y e. x -> y e. w ) ) ) -> E. x A. y -. y e. x )
12		ax-tco	|- E. w ( z e. w /\ A. x ( x e. w -> A. y ( y e. x -> y e. w ) ) )
13	11 12	exlimiiv	|- E. x A. y -. y e. x