Description: Define unordered pair of classes. Definition 7.1 of Quine p. 48. For
example, A e. { 1 , -u 1 } -> ( A ^ 2 ) = 1 ( ex-pr ). They are
unordered, so { A , B } = { B , A } as proven by prcom . For a more
traditional definition, but requiring a dummy variable, see dfpr2 .
{ A , A } is also an unordered pair, but also a singleton because of
{ A } = { A , A } (see dfsn2 ). Therefore, { A , B } is called
aproper (unordered) pair iff A =/= B and A and B are sets.

Note: ordered pairs are a completely different object defined below in
df-op . When the term "pair" is used without qualifier, it generally
means "unordered pair", and the context makes it clear which version is
meant. (Contributed by NM, 21-Jun-1993)