Description: Equivalence for an ordered pair of two identical singletons equal to a singleton of an ordered pair. (Contributed by AV, 24-Sep-2020) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)