Metamath Proof Explorer

Theorem wl-sb8eut

Description: Substitution of variable in universal quantifier. Closed form of sb8eu . (Contributed by Wolf Lammen, 11-Aug-2019)

Ref Expression
Assertion wl-sb8eut ⊢ ∀ 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 nfa1 ⊢ Ⅎ x ∀ x Ⅎ y φ
6 sp ⊢ ∀ x Ⅎ y φ → Ⅎ y φ
7 5 6 nfsbd ⊢ ∀ x Ⅎ y φ → Ⅎ y v x φ
8 nfvd ⊢ ∀ x Ⅎ y φ → Ⅎ y v = u
9 7 8 nfbid ⊢ ∀ x Ⅎ y φ → Ⅎ y v x φ ↔ v = u
10 4 9 nfxfrd ⊢ ∀ x Ⅎ y φ → Ⅎ y v x φ ↔ x = u
11 sbequ ⊢ v = y → v x φ ↔ x = u ↔ y x φ ↔ x = u
12 11 a1i ⊢ ∀ x Ⅎ y φ → v = y → v x φ ↔ x = u ↔ y x φ ↔ x = u
13 2 10 12 cbvald ⊢ ∀ x Ⅎ y φ → ∀ v v x φ ↔ x = u ↔ ∀ y y x φ ↔ x = u
14 nfv ⊢ Ⅎ v φ ↔ x = u
15 14 sb8 ⊢ ∀ x φ ↔ x = u ↔ ∀ v v x φ ↔ x = u
16 15 bicomi ⊢ ∀ v v x φ ↔ x = u ↔ ∀ x φ ↔ x = u
17 equsb3 ⊢ y x x = u ↔ y = u
18 17 sblbis ⊢ y x φ ↔ x = u ↔ y x φ ↔ y = u
19 18 albii ⊢ ∀ y y x φ ↔ x = u ↔ ∀ y y x φ ↔ y = u
20 13 16 19 3bitr3g ⊢ ∀ x Ⅎ y φ → ∀ x φ ↔ x = u ↔ ∀ y y x φ ↔ y = u
21 20 exbidv ⊢ ∀ x Ⅎ y φ → ∃ u ∀ x φ ↔ x = u ↔ ∃ u ∀ y y x φ ↔ y = u
22 eu6 ⊢ ∃! x φ ↔ ∃ u ∀ x φ ↔ x = u
23 eu6 ⊢ ∃! y y x φ ↔ ∃ u ∀ y y x φ ↔ y = u
24 21 22 23 3bitr4g ⊢ ∀ x Ⅎ y φ → ∃! x φ ↔ ∃! y y x φ