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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-pr | ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) |
| 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 | ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) |