Metamath Proof Explorer

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

Proof

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