Description: Equivalence of an "at most one" and an "at most one" restricted to the domain inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021)