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

Proof

Step Hyp Ref Expression
1 zfregs2 ⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ → ¬ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) )
2 abn0 ⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
3 df-ral ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) )
4 3 notbii ⊢ ( ¬ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ¬ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) )
5 exnal ⊢ ( ∃ 𝑦 ¬ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) ↔ ¬ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) )
6 annim ⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∧ ¬ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) ↔ ¬ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) )
7 df-clab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
8 sb6 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
9 7 8 bitri ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
10 df-clab ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] 𝜑 )
11 sb6 ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
12 10 11 bitri ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
13 12 anbi2ci ⊢ ( ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
14 df-an ⊢ ( ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ↔ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
15 13 14 bitri ⊢ ( ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
16 15 con2bii ⊢ ( ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ↔ ¬ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) )
17 16 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ↔ ∀ 𝑧 ¬ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) )
18 alnex ⊢ ( ∀ 𝑧 ¬ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ¬ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) )
19 17 18 bitr2i ⊢ ( ¬ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
20 9 19 anbi12i ⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∧ ¬ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
21 6 20 bitr3i ⊢ ( ¬ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
22 21 exbii ⊢ ( ∃ 𝑦 ¬ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
23 4 5 22 3bitr2i ⊢ ( ¬ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
24 1 2 23 3imtr3i ⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )