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 nfv ⊢ Ⅎ w φ ↔ x = z
3 2 sb8v ⊢ ∀ x φ ↔ x = z ↔ ∀ w w x φ ↔ x = z
4 equsb3 ⊢ w x x = z ↔ w = z
5 4 sblbis ⊢ w x φ ↔ x = z ↔ w x φ ↔ w = z
6 5 albii ⊢ ∀ w w x φ ↔ x = z ↔ ∀ w w x φ ↔ w = z
7 nfv ⊢ Ⅎ y w = z
8 1 7 nfbi ⊢ Ⅎ y w x φ ↔ w = z
9 nfv ⊢ Ⅎ w y x φ ↔ y = z
10 sbequ ⊢ w = y → w x φ ↔ y x φ
11 equequ1 ⊢ w = y → w = z ↔ y = z
12 10 11 bibi12d ⊢ w = y → w x φ ↔ w = z ↔ y x φ ↔ y = z
13 8 9 12 cbvalv1 ⊢ ∀ w w x φ ↔ w = z ↔ ∀ y y x φ ↔ y = z
14 3 6 13 3bitri ⊢ ∀ x φ ↔ x = z ↔ ∀ y y x φ ↔ y = z
15 14 exbii ⊢ ∃ z ∀ x φ ↔ x = z ↔ ∃ z ∀ y y x φ ↔ y = z
16 eu6 ⊢ ∃! x φ ↔ ∃ z ∀ x φ ↔ x = z
17 eu6 ⊢ ∃! y y x φ ↔ ∃ z ∀ y y x φ ↔ y = z
18 15 16 17 3bitr4i ⊢ ∃! x φ ↔ ∃! y y x φ