Theorem axregszf

Description: Derivation of zfregs using ax-regs . (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	axregszf	|- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. x x e. A )
2		axregscl	|- ( E. x x e. A -> E. x ( x e. A /\ A. y ( y e. x -> -. y e. A ) ) )
3		disj1	|- ( ( x i^i A ) = (/) <-> A. y ( y e. x -> -. y e. A ) )
4	3	rexbii	|- ( E. x e. A ( x i^i A ) = (/) <-> E. x e. A A. y ( y e. x -> -. y e. A ) )
5		df-rex	|- ( E. x e. A A. y ( y e. x -> -. y e. A ) <-> E. x ( x e. A /\ A. y ( y e. x -> -. y e. A ) ) )
6	4 5	bitr2i	|- ( E. x ( x e. A /\ A. y ( y e. x -> -. y e. A ) ) <-> E. x e. A ( x i^i A ) = (/) )
7	2 6	sylib	|- ( E. x x e. A -> E. x e. A ( x i^i A ) = (/) )
8	1 7	sylbi	|- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )