Metamath Proof Explorer

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 ⊢ ∃ x x ∈ A → ∃ y y ∈ A ∧ ∀ z z ∈ y → ¬ z ∈ A

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ x = w → x ∈ A ↔ w ∈ A
2 1 cbvexvw ⊢ ∃ x x ∈ A ↔ ∃ w w ∈ A
3 ax-regs ⊢ ∃ w w ∈ A → ∃ y ∀ w w = y → w ∈ A ∧ ∀ z z ∈ y → ¬ ∀ w w = z → w ∈ A
4 eleq1w ⊢ w = y → w ∈ A ↔ y ∈ A
5 4 equsalvw ⊢ ∀ w w = y → w ∈ A ↔ y ∈ A
6 eleq1w ⊢ w = z → w ∈ A ↔ z ∈ A
7 6 equsalvw ⊢ ∀ w w = z → w ∈ A ↔ z ∈ A
8 7 notbii ⊢ ¬ ∀ w w = z → w ∈ A ↔ ¬ z ∈ A
9 8 imbi2i ⊢ z ∈ y → ¬ ∀ w w = z → w ∈ A ↔ z ∈ y → ¬ z ∈ A
10 9 albii ⊢ ∀ z z ∈ y → ¬ ∀ w w = z → w ∈ A ↔ ∀ z z ∈ y → ¬ z ∈ A
11 5 10 anbi12i ⊢ ∀ w w = y → w ∈ A ∧ ∀ z z ∈ y → ¬ ∀ w w = z → w ∈ A ↔ y ∈ A ∧ ∀ z z ∈ y → ¬ z ∈ A
12 11 exbii ⊢ ∃ y ∀ w w = y → w ∈ A ∧ ∀ z z ∈ y → ¬ ∀ w w = z → w ∈ A ↔ ∃ y y ∈ A ∧ ∀ z z ∈ y → ¬ z ∈ A
13 3 12 sylib ⊢ ∃ w w ∈ A → ∃ y y ∈ A ∧ ∀ z z ∈ y → ¬ z ∈ A
14 2 13 sylbi ⊢ ∃ x x ∈ A → ∃ y y ∈ A ∧ ∀ z z ∈ y → ¬ z ∈ A