Metamath Proof Explorer

Theorem regsfromsetind

Description: Derivation of ax-regs from mh-setind . (Contributed by Matthew House, 4-Mar-2026)

Ref Expression
Hypothesis regsfromsetind.1 ⊢ ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ → ¬ φ
Assertion regsfromsetind ⊢ ∃ x φ → ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ

Proof

Step Hyp Ref Expression
1 regsfromsetind.1 ⊢ ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ → ¬ φ
2 nfia1 ⊢ Ⅎ x ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ
3 2 nfal ⊢ Ⅎ x ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ
4 3 nfn ⊢ Ⅎ x ¬ ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ
5 1 con2i ⊢ φ → ¬ ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ
6 4 5 exlimi ⊢ ∃ x φ → ¬ ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ
7 exnalimn ⊢ ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ ↔ ¬ ∀ y ∀ x x = y → φ → ¬ ∀ z z ∈ y → ¬ ∀ x x = z → φ
8 nfv ⊢ Ⅎ z x ∈ y → ¬ φ
9 nfv ⊢ Ⅎ x z ∈ y
10 nfna1 ⊢ Ⅎ x ¬ ∀ x x = z → φ
11 9 10 nfim ⊢ Ⅎ x z ∈ y → ¬ ∀ x x = z → φ
12 elequ1 ⊢ x = z → x ∈ y ↔ z ∈ y
13 sbequ12 ⊢ x = z → φ ↔ z x φ
14 sb6 ⊢ z x φ ↔ ∀ x x = z → φ
15 13 14 bitrdi ⊢ x = z → φ ↔ ∀ x x = z → φ
16 15 notbid ⊢ x = z → ¬ φ ↔ ¬ ∀ x x = z → φ
17 12 16 imbi12d ⊢ x = z → x ∈ y → ¬ φ ↔ z ∈ y → ¬ ∀ x x = z → φ
18 8 11 17 cbvalv1 ⊢ ∀ x x ∈ y → ¬ φ ↔ ∀ z z ∈ y → ¬ ∀ x x = z → φ
19 alinexa ⊢ ∀ x x = y → ¬ φ ↔ ¬ ∃ x x = y ∧ φ
20 sbalex ⊢ ∃ x x = y ∧ φ ↔ ∀ x x = y → φ
21 19 20 xchbinx ⊢ ∀ x x = y → ¬ φ ↔ ¬ ∀ x x = y → φ
22 18 21 imbi12i ⊢ ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ ↔ ∀ z z ∈ y → ¬ ∀ x x = z → φ → ¬ ∀ x x = y → φ
23 con2b ⊢ ∀ z z ∈ y → ¬ ∀ x x = z → φ → ¬ ∀ x x = y → φ ↔ ∀ x x = y → φ → ¬ ∀ z z ∈ y → ¬ ∀ x x = z → φ
24 22 23 bitri ⊢ ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ ↔ ∀ x x = y → φ → ¬ ∀ z z ∈ y → ¬ ∀ x x = z → φ
25 24 albii ⊢ ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ ↔ ∀ y ∀ x x = y → φ → ¬ ∀ z z ∈ y → ¬ ∀ x x = z → φ
26 7 25 xchbinxr ⊢ ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ ↔ ¬ ∀ y ∀ x x ∈ y → ¬ φ → ∀ x x = y → ¬ φ
27 6 26 sylibr ⊢ ∃ x φ → ∃ y ∀ x x = y → φ ∧ ∀ z z ∈ y → ¬ ∀ x x = z → φ