Definition df-pr

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. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Assertion	df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cpr	⊢ { 𝐴 , 𝐵 }
3	0	csn	⊢ { 𝐴 }
4	1	csn	⊢ { 𝐵 }
5	3 4	cun	⊢ ( { 𝐴 } ∪ { 𝐵 } )
6	2 5	wceq	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )