Description: Lemma for renegeu and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023)