Metamath Proof Explorer

Theorem sb8eulem

Description: Lemma. Factor out the common proof skeleton of sb8euv and sb8eu . Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 24-Aug-2019) Factor out common proof lines. (Revised by Wolf Lammen, 9-Feb-2023)

Ref Expression
Hypothesis sb8eulem.nfsb ⊢ Ⅎ y w x φ
Assertion sb8eulem ⊢ ∃! x φ ↔ ∃! y y x φ

Proof

Step Hyp Ref Expression
1 sb8eulem.nfsb ⊢ Ⅎ y w x φ
2 sb8v ⊢ ∀ x φ ↔ x = z ↔ ∀ w w x φ ↔ x = z
3 equsb3 ⊢ w x x = z ↔ w = z
4 3 sblbis ⊢ w x φ ↔ x = z ↔ w x φ ↔ w = z
5 4 albii ⊢ ∀ w w x φ ↔ x = z ↔ ∀ w w x φ ↔ w = z
6 nfv ⊢ Ⅎ y w = z
7 1 6 nfbi ⊢ Ⅎ y w x φ ↔ w = z
8 nfv ⊢ Ⅎ w y x φ ↔ y = z
9 sbequ ⊢ w = y → w x φ ↔ y x φ
10 equequ1 ⊢ w = y → w = z ↔ y = z
11 9 10 bibi12d ⊢ w = y → w x φ ↔ w = z ↔ y x φ ↔ y = z
12 7 8 11 cbvalv1 ⊢ ∀ w w x φ ↔ w = z ↔ ∀ y y x φ ↔ y = z
13 2 5 12 3bitri ⊢ ∀ x φ ↔ x = z ↔ ∀ y y x φ ↔ y = z
14 13 exbii ⊢ ∃ z ∀ x φ ↔ x = z ↔ ∃ z ∀ y y x φ ↔ y = z
15 eu6 ⊢ ∃! x φ ↔ ∃ z ∀ x φ ↔ x = z
16 eu6 ⊢ ∃! y y x φ ↔ ∃ z ∀ y y x φ ↔ y = z
17 14 15 16 3bitr4i ⊢ ∃! x φ ↔ ∃! y y x φ