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	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1w	⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
2	1	cbvexvw	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑤 𝑤 ∈ 𝐴 )
3		ax-regs	⊢ ( ∃ 𝑤 𝑤 ∈ 𝐴 → ∃ 𝑦 ( ∀ 𝑤 ( 𝑤 = 𝑦 → 𝑤 ∈ 𝐴 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑤 ( 𝑤 = 𝑧 → 𝑤 ∈ 𝐴 ) ) ) )
4		eleq1w	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
5	4	equsalvw	⊢ ( ∀ 𝑤 ( 𝑤 = 𝑦 → 𝑤 ∈ 𝐴 ) ↔ 𝑦 ∈ 𝐴 )
6		eleq1w	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
7	6	equsalvw	⊢ ( ∀ 𝑤 ( 𝑤 = 𝑧 → 𝑤 ∈ 𝐴 ) ↔ 𝑧 ∈ 𝐴 )
8	7	notbii	⊢ ( ¬ ∀ 𝑤 ( 𝑤 = 𝑧 → 𝑤 ∈ 𝐴 ) ↔ ¬ 𝑧 ∈ 𝐴 )
9	8	imbi2i	⊢ ( ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑤 ( 𝑤 = 𝑧 → 𝑤 ∈ 𝐴 ) ) ↔ ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴 ) )
10	9	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑤 ( 𝑤 = 𝑧 → 𝑤 ∈ 𝐴 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴 ) )
11	5 10	anbi12i	⊢ ( ( ∀ 𝑤 ( 𝑤 = 𝑦 → 𝑤 ∈ 𝐴 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑤 ( 𝑤 = 𝑧 → 𝑤 ∈ 𝐴 ) ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴 ) ) )
12	11	exbii	⊢ ( ∃ 𝑦 ( ∀ 𝑤 ( 𝑤 = 𝑦 → 𝑤 ∈ 𝐴 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑤 ( 𝑤 = 𝑧 → 𝑤 ∈ 𝐴 ) ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴 ) ) )
13	3 12	sylib	⊢ ( ∃ 𝑤 𝑤 ∈ 𝐴 → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴 ) ) )
14	2 13	sylbi	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴 ) ) )