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