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 ⊢Ⅎywxφ
Assertion sb8eulem ⊢∃!xφ↔∃!yyxφ

Proof

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