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)