Metamath Proof Explorer

Theorem wl-sb8eutv

Description: Substitution of variable in universal quantifier. Closed form of sb8euv . (Contributed by Wolf Lammen, 3-May-2025)

Ref Expression
Assertion wl-sb8eutv ⊢ ∀ x Ⅎ y φ → ∃! x φ ↔ ∃! y y x φ

Proof

Step Hyp Ref Expression
1 nfnf1 ⊢ Ⅎ y Ⅎ y φ
2 1 nfal ⊢ Ⅎ y ∀ x Ⅎ y φ
3 equsb3 ⊢ v x x = u ↔ v = u
4 3 sblbis ⊢ v x φ ↔ x = u ↔ v x φ ↔ v = u
5 wl-nfsbtv ⊢ ∀ x Ⅎ y φ → Ⅎ y v x φ
6 nfvd ⊢ ∀ x Ⅎ y φ → Ⅎ y v = u
7 5 6 nfbid ⊢ ∀ x Ⅎ y φ → Ⅎ y v x φ ↔ v = u
8 4 7 nfxfrd ⊢ ∀ x Ⅎ y φ → Ⅎ y v x φ ↔ x = u
9 sbequ ⊢ v = y → v x φ ↔ x = u ↔ y x φ ↔ x = u
10 9 a1i ⊢ ∀ x Ⅎ y φ → v = y → v x φ ↔ x = u ↔ y x φ ↔ x = u
11 2 8 10 cbvaldw ⊢ ∀ x Ⅎ y φ → ∀ v v x φ ↔ x = u ↔ ∀ y y x φ ↔ x = u
12 sb8v ⊢ ∀ x φ ↔ x = u ↔ ∀ v v x φ ↔ x = u
13 12 bicomi ⊢ ∀ v v x φ ↔ x = u ↔ ∀ x φ ↔ x = u
14 equsb3 ⊢ y x x = u ↔ y = u
15 14 sblbis ⊢ y x φ ↔ x = u ↔ y x φ ↔ y = u
16 15 albii ⊢ ∀ y y x φ ↔ x = u ↔ ∀ y y x φ ↔ y = u
17 11 13 16 3bitr3g ⊢ ∀ x Ⅎ y φ → ∀ x φ ↔ x = u ↔ ∀ y y x φ ↔ y = u
18 17 exbidv ⊢ ∀ x Ⅎ y φ → ∃ u ∀ x φ ↔ x = u ↔ ∃ u ∀ y y x φ ↔ y = u
19 eu6 ⊢ ∃! x φ ↔ ∃ u ∀ x φ ↔ x = u
20 eu6 ⊢ ∃! y y x φ ↔ ∃ u ∀ y y x φ ↔ y = u
21 18 19 20 3bitr4g ⊢ ∀ x Ⅎ y φ → ∃! x φ ↔ ∃! y y x φ