Metamath Proof Explorer

Theorem axregs

Description: Derivation of ax-regs from the axioms of ZF set theory. (Contributed by BTernaryTau, 29-Dec-2025)

Ref Expression
Assertion axregs ⊢ ∃ x φ → ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ

Proof

Step Hyp Ref Expression
1 zfregs2 ⊢ x | φ ≠ ∅ → ¬ ∀ y ∈ x | φ ∃ z z ∈ x | φ ∧ z ∈ y
2 abn0 ⊢ x | φ ≠ ∅ ↔ ∃ x φ
3 df-ral ⊢ ∀ y ∈ x | φ ∃ z z ∈ x | φ ∧ z ∈ y ↔ ∀ y y ∈ x | φ → ∃ z z ∈ x | φ ∧ z ∈ y
4 3 notbii ⊢ ¬ ∀ y ∈ x | φ ∃ z z ∈ x | φ ∧ z ∈ y ↔ ¬ ∀ y y ∈ x | φ → ∃ z z ∈ x | φ ∧ z ∈ y
5 exnal ⊢ ∃ y ¬ y ∈ x | φ → ∃ z z ∈ x | φ ∧ z ∈ y ↔ ¬ ∀ y y ∈ x | φ → ∃ z z ∈ x | φ ∧ z ∈ y
6 annim ⊢ y ∈ x | φ ∧ ¬ ∃ z z ∈ x | φ ∧ z ∈ y ↔ ¬ y ∈ x | φ → ∃ z z ∈ x | φ ∧ z ∈ y
7 df-clab ⊢ y ∈ x | φ ↔ y x φ
8 sb6 ⊢ y x φ ↔ ∀ x x = y → φ
9 7 8 bitri ⊢ y ∈ x | φ ↔ ∀ x x = y → φ
10 df-clab ⊢ z ∈ x | φ ↔ z x φ
11 sb6 ⊢ z x φ ↔ ∀ x x = z → φ
12 10 11 bitri ⊢ z ∈ x | φ ↔ ∀ x x = z → φ
13 12 anbi2ci ⊢ z ∈ x | φ ∧ z ∈ y ↔ z ∈ y ∧ ∀ x x = z → φ
14 df-an ⊢ z ∈ y ∧ ∀ x x = z → φ ↔ ¬ z ∈ y → ¬ ∀ x x = z → φ
15 13 14 bitri ⊢ z ∈ x | φ ∧ z ∈ y ↔ ¬ z ∈ y → ¬ ∀ x x = z → φ
16 15 con2bii ⊢ z ∈ y → ¬ ∀ x x = z → φ ↔ ¬ z ∈ x | φ ∧ z ∈ y
17 16 albii ⊢ ∀ z z ∈ y → ¬ ∀ x x = z → φ ↔ ∀ z ¬ z ∈ x | φ ∧ z ∈ y
18 alnex ⊢ ∀ z ¬ z ∈ x | φ ∧ z ∈ y ↔ ¬ ∃ z z ∈ x | φ ∧ z ∈ y
19 17 18 bitr2i ⊢ ¬ ∃ z z ∈ x | φ ∧ z ∈ y ↔ ∀ z z ∈ y → ¬ ∀ x x = z → φ
20 9 19 anbi12i ⊢ y ∈ x | φ ∧ ¬ ∃ z z ∈ x | φ ∧ z ∈ y ↔ ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ
21 6 20 bitr3i ⊢ ¬ y ∈ x | φ → ∃ z z ∈ x | φ ∧ z ∈ y ↔ ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ
22 21 exbii ⊢ ∃ y ¬ y ∈ x | φ → ∃ z z ∈ x | φ ∧ z ∈ y ↔ ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ
23 4 5 22 3bitr2i ⊢ ¬ ∀ y ∈ x | φ ∃ z z ∈ x | φ ∧ z ∈ y ↔ ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ
24 1 2 23 3imtr3i ⊢ ∃ x φ → ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ