Description: There is a unique proper unordered pair over a given set V fulfilling a wff iff there is a unique subset of V of size two fulfilling this wff. (Contributed by AV, 29-Apr-2023)