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 φ