Great question! Let's work through this proof using the standard set-theoretic definition of ordered pairs—this is the key to formalizing the intuition that ordered pairs have a unique "first" and "second" element.

Step 1: Recall the Kuratowski Definition of Ordered Pairs #

First, we start with the widely accepted Kuratowski definition, which grounds ordered pairs in basic set theory:
(A, B) = {{A}, {A, B}}
This definition encodes the order of elements by using nested sets: the singleton {A} identifies the first element, and the pair {A, B} links it to the second.

Step 2: Use Set Equality Definition #

We know (A, B) = (C, D), which translates to:
{{A}, {A, B}} = {{C}, {C, D}}
By the definition of set equality, two sets are equal if and only if they contain exactly the same elements. So every element in the left set must be in the right set, and vice versa. We'll split this into two cases based on whether A = B or A ≠ B.

Case 1: A = B

If A = B, then:
(A, B) = {{A}, {A, A}} = {{A}, {A}} = {{A}}
Since (A, B) = (C, D), this means {{A}} = {{C}, {C, D}}. A set with only one element ({A}) can only equal another set if that set also has exactly one element. So {C} = {C, D}, which implies C = D. Now we have {{A}} = {{C}}, so {A} = {C}, which gives A = C. Since A = B and C = D, we conclude A = C ∧ B = D.

Case 2: A ≠ B

Here, the set {{A}, {A, B}} has two distinct elements (because A ≠ B, so {A} ≠ {A, B}). For this to equal {{C}, {C, D}}, the elements must match in one of two ways:

• Subcase 2a: {A} = {C} and {A, B} = {C, D}
  From {A} = {C}, we get A = C. Substitute into the second equality: {A, B} = {A, D}. Since A ≠ B, the only way these sets are equal is if B = D. Thus, A = C ∧ B = D.
• Subcase 2b: {A} = {C, D} and {A, B} = {C}
  From {A, B} = {C}, we know both A = C and B = C, so A = B. But this contradicts our initial assumption that A ≠ B, so this subcase is impossible.

Step 3: Conclusion #

In both valid cases, we end up with A = C and B = D. This confirms that ordered pairs are uniquely determined by their first and second elements.

Note: While the Kuratowski definition is standard, other definitions of ordered pairs exist (e.g., Wiener's definition), but all of them are constructed to satisfy this core "uniqueness" property. In some contexts, this property is even taken as the definition of ordered pairs, since it captures exactly what we need them to do.

内容的提问来源于stack exchange，提问作者radrow