Theorem axreg

Description: Derivation of ax-reg from ax-regs and Tarski's FOL axiom schemes. This demonstrates the sense in which ax-regs is a stronger version of ax-reg . (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	axreg	|- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-regs	|- ( E. w w e. x -> E. y ( A. w ( w = y -> w e. x ) /\ A. z ( z e. y -> -. A. w ( w = z -> w e. x ) ) ) )
2		elequ1	|- ( w = y -> ( w e. x <-> y e. x ) )
3	2	cbvexvw	|- ( E. w w e. x <-> E. y y e. x )
4	2	equsalvw	|- ( A. w ( w = y -> w e. x ) <-> y e. x )
5		elequ1	|- ( w = z -> ( w e. x <-> z e. x ) )
6	5	equsalvw	|- ( A. w ( w = z -> w e. x ) <-> z e. x )
7	6	notbii	|- ( -. A. w ( w = z -> w e. x ) <-> -. z e. x )
8	7	imbi2i	|- ( ( z e. y -> -. A. w ( w = z -> w e. x ) ) <-> ( z e. y -> -. z e. x ) )
9	8	albii	|- ( A. z ( z e. y -> -. A. w ( w = z -> w e. x ) ) <-> A. z ( z e. y -> -. z e. x ) )
10	4 9	anbi12i	|- ( ( A. w ( w = y -> w e. x ) /\ A. z ( z e. y -> -. A. w ( w = z -> w e. x ) ) ) <-> ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )
11	10	exbii	|- ( E. y ( A. w ( w = y -> w e. x ) /\ A. z ( z e. y -> -. A. w ( w = z -> w e. x ) ) ) <-> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )
12	1 3 11	3imtr3i	|- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )