Theorem axregscl

Description: A version of ax-regs with a class variable instead of a wff variable. Axiom D in Gödel,The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory (1940), p. 6. (Contributed by BTernaryTau, 30-Dec-2025)

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

Proof

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