nyuuzyou/wikis huggingface dataset:
Equality Relation is Primitive Recursive

== Theorem ==
The relation $\operatorname{eq} \subseteq \N^2$, defined as:
:$\map {\operatorname {eq} } {n, m} \iff n = m$
is primitive recursive.
== Proof ==
We note that:
:$n = m \iff \size {n - m} = 0$
:$n \ne m \iff \size {n - m} > 0$
So it can be seen that the characteristic function of $\operatorname{eq}$ is given by:
:$\map {\chi_{\operatorname {eq} } } {n, m} = \overline {\map \sgn {\map {\operatorname {adf} } {n, m} } }$.
So $\map {\chi_{\operatorname {eq} } } {n, m}$ is defined by substitution from:
:the primitive recursive function $\overline \sgn$
:the primitive recursive function $\operatorname {adf}$.
Thus $\chi_{\operatorname {eq} }$ is primitive recursive.
Hence the result.
Category:Primitive Recursive Functions
Equality implies Substitution

== Theorem ==
Let $\map P x$ denote a Well-Formed Formula which contains $x$ as a free variable.
Then the following are tautologies:
:$\forall x: \paren {\map P x \iff \exists y: \paren {y = x \land \map P y} }$
:$\forall x: \paren {\map P x \iff \forall y: \paren {y = x \implies \map P y} }$
Note that when $y$ is substituted for $x$ in either formula, it is false in general; compare Confusion of Bound Variables.
== Proof ==
By Universal Affirmative implies Particular Affirmative iff First Predicate is not Vacuous:
:$\paren {\exists y: y = x \land \forall y: \paren {y = x \implies \map P x} } \implies \exists y: \paren {y = x \land \map P x}$
Then:
Similarly:
The above two statements comprise the other direction of the biconditional assertions.
Together, $(1)$, $(2)$, $(3)$, and $(4)$ prove the two assertions.
== Sources ==
* : $\S 6.1$
* : $\S 6.2$
Category:Predicate Logic
Equality is Reflexive

== Theorem ==
Equality is reflexive.
That is:
:$\forall a: a = a$
== Proof ==
This proof depends on Leibniz's law:
:$x = y \dashv \vdash \map P x \iff \map P y$
We are trying to prove $a = a$.
Our assertion, then, is:
:$a = a \dashv \vdash \map P a \iff \map P a$
From Law of Identity, $\map P a \iff \map P a$ is a tautology.
Thus $a = a$ is also tautologous, and the theorem holds.
== Also see ==
* Equality is Symmetric
* Equality is Transitive
* Equality is Equivalence Relation
== Sources ==
* : Chapter $3$
* : $\S 1$: The Axiom of Extension
* : Introduction: Review of Algebra, Geometry, and Trigonometry: $\text{0-1}$: The Real Numbers
* : $\S 3.2$
* : $\S 1$: Some mathematical language: Equality: $\text{(a)}$
Category:Logic
Category:Equality
Equality is Symmetric

== Theorem ==
Equality is symmetric.
That is:
:$\forall a, b: a = b \implies b = a$
== Proof ==
== Also see ==
* Equality is Reflexive
* Equality is Transitive
* Equality is Equivalence Relation
== Sources ==
* : Chapter $3$
* : $\S 1$: The Axiom of Extension
* : Introduction: Review of Algebra, Geometry, and Trigonometry: $\text{0-1}$: The Real Numbers
* : $\S 3.2$
* : $\S 1$: Some mathematical language: Equality: $\text{(b)}$
Category:Logic
Category:Equality
Equality is Transitive

== Theorem ==
Equality is transitive:
:$\forall a, b, c: \paren {a = b} \land \paren {b = c} \implies a = c$
== Proof ==
== Also see ==
* Equality is Reflexive
* Equality is Symmetric
* Equality is Equivalence Relation
== Sources ==
* : $\S 1$: The Axiom of Extension
* : Introduction: Review of Algebra, Geometry, and Trigonometry: $\text{0-1}$: The Real Numbers
* : $\S 3.2$
* : $\S 1$: Some mathematical language: Equality: $\text{(c)}$
Category:Logic
Category:Equality
Equality of Algebraic Structures

== Theorem ==
Two algebraic structures $\struct {S, \circ}$ and $\struct {T, *}$ are equal :
:$S = T$
:$\forall a, b \in S: a \circ b = a * b$
== Proof ==
This follows from set equality and Equality of Ordered Pairs.
Category:Algebraic Structures
Category:Equality
Equality of Cartesian Products

== Theorem ==
Let $A, B, C, D$ be nonempty sets.
Then:
:$A \times B = C \times D \iff A = C \land B = D$
where $\times$ denotes cartesian product.
== Proof ==
If $A = C$ and $B = D$, it is immediate that $A \times B = C \times D$.
Now suppose that $A \times B = C \times D$.
By definition of Cartesian product:
It follows that $x \in A$ $x \in C$, and so $A = C$.
Similarly, $y \in B$ $y \in D$, hence $B = D$.
The result follows.
== Also see ==
* Cartesian Product is not Associative
Category:Cartesian Product
Category:Equality
Equality of Complex Numbers

== Theorem ==
Let $z_1 := a_1 + i b_1$ and $z_2 := a_2 + i b_2$ be complex numbers.
Then $z_1 = z_2$ $a_1 = a_2$ and $b_1 = b_2$.
== Proof ==
By definition of a complex number, $z_1$ and $z_2$ can be expressed in the form:
:$z_1 = \tuple {a_1, b_1}$
:$z_2 = \tuple {a_2, b_2}$
where $\tuple {a, b}$ denotes an ordered pair.
The result follows from Equality of Ordered Pairs.
== Sources ==
* : Chapter $\text I$: Functions of a Complex Variable: $\S 1$. Complex Numbers: $\text {(i)}$
* : $\S 1.2$. The Algebraic Theory
* : $\S 6$: Complex Numbers: Equality of Complex Numbers: $6.1$
* : $1$: Complex Numbers: The Complex Number System
* : $1$: Complex Numbers: Axiomatic Foundations of the Complex Number System: $\text {A}$. Equality
* : $1$ The complex plane: Complex numbers $\S 1.1$ Complex numbers and their representation
* : $\S 4$: Complex Numbers: Equality of Complex Numbers: $4.1.$
Category:Complex Numbers
Category:Equality
Equality of Cycles

== Theorem ==
Let $S_n$ denote the symmetric group on $n$ letters, realised as the permutations of $\set {1, \ldots, n}$.
Let:
:$\rho = \begin {bmatrix} a_0 & \cdots & a_{k - 1} \end {bmatrix} \in S_n$
:$\sigma = \begin {bmatrix} b_0 & \cdots & b_{k - 1} \end {bmatrix} \in S_n$
be $k$-cycles of $S_n$.
For $d \in \Z$, by Integer is Congruent to Integer less than Modulus we can associate to $d$ a unique integer $\tilde d \in \set {0, \ldots, k - 1}$ such that:
:$d \equiv \tilde d \pmod k$
Define $a_d$ and $b_d$ for any $d \in \Z$ by $a_d = a_{\tilde d}$ and $b_d = b_{\tilde d}$
Choose $i, j \in \set {1, \ldots, k}$ such that:
:$\ds a_i = \min \set {a_0, \ldots, a_{k - 1} }$
:$\ds b_j = \min \set {b_0, \ldots, b_{k - 1} }$
Then:
:$\rho = \sigma$
:
:$\forall d \in \Z: a_{i + d} = b_{j + d}$
That is, $\rho = \sigma$ they are identical when written with the lowest element first.
== Proof ==
Category:Symmetric Groups
Equality of Division Products

== Theorem ==
Let $\struct {R, +, \circ}$ be a commutative ring with unity.
Let $\struct {U_R, \circ}$ be the group of units of $\struct {R, +, \circ}$.
Let $a, b \in R, c, d \in U_R$.
Then:
:$\dfrac a c = \dfrac b d \iff a \circ d = b \circ c$
where $\dfrac x z$ is defined as $x \circ \paren {z^{-1} }$, that is, $x$ divided by $z$.
== Proof ==
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $23$. The Field of Rational Numbers: Theorem $23.7 \ (3)$
Category:Commutative Algebra
Equality of Elements in Range of Mapping

== Theorem ==
Let $f: S \to T$ be a mapping.
Then:
:$\exists y \in \Rng f: \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f \iff \map f {x_1} = \map f {x_2}$
== Proof ==
=== Necessary Condition ===
Let:
:$\exists y \in \Rng f: \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f$
Then:
=== Sufficient Condition ===
Let:
:$\map f {x_1} = \map f {x_2}$
Then:
The result follows from the definition of logical equivalence.
Category:Mapping Theory
Equality of Integers to the Power of Each Other

== Theorem ==
$2$ and $4$ are the only pair of positive integers $m, n$ such that $m \ne n$ such that:
:$m^n = n^m$
Thus:
$2^4 = 4^2 = 16$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $16$
* : $16$
Category:16
Category:Number Theory
Category:Equality of Integers to the Power of Each Other
Equality of Integers to the Power of Each Other/Proof 1

== Theorem ==
== Proof ==
We have:
, let $m > n$.
We have that $m, n \in \N$.
Hence:
:$\log_n m \in \N \implies m = n^k$
where $k \in \N_{>1}$ .
Hence:
:$n^k = k n$
For $n \ne 0$ the solution reads 
:$n = k^\frac 1 {k - 1}$
Define $t = k - 1$.
We have:
To check for intermediate maximum consider the first derivative:
:$\dfrac {\d n} {\d k} = \dfrac {k^{\frac 1 {k - 1} } } {k - 1} \paren {\dfrac 1 k - \dfrac {\ln k} {k - 1} }$
Our desired solution constrains the prefactor to be positive.
The term in brackets vanishes only for $k = 1$.
Hence for $k > 1$:
:there is no extremum
:$\map n k$ is monotonically decreasing
:$1 < n < e$.
Hence the only natural number solution is $n = 2$.
The only $k$ that satisfies this is $k = 2$.
Therefore:
:$n = 2$
:$m = 2^2 = 4$
Category:Equality of Integers to the Power of Each Other
Equality of Integers to the Power of Each Other/Proof 2

== Theorem ==
== Proof ==
 suppose $m > n$.
Write $m = n + x$, where $x$ is an integer.
Then:
From Real Sequence $\paren {1 + \dfrac x n}^n$ is Convergent:
:$\paren {1 + \dfrac x n}^n$ is increasing and has limit $e^x$.
Hence:
:$n^x < e^x$
This forces $n = 2$.
We have:
:$m^2 = 2^m$
showing that $m$ is a power of $2$.
Write $m = 2^k$. 
Then:
:$2^{2 k} = 2^{2^k}$
giving:
:$k = 2^{k - 1}$
By Bernoulli's Inequality:
:$2^{k - 1} \ge 1 + k - 1 = k$
where equality holds $k - 1 = 0$ or $k - 1 = 1$.
We can skip Bernoulli's Inequality by induction on $k$ for $k > 2$.
Either way, this gives:
:$k = 1$ or $2$
:$m = 2$ or $4$.
We reject $m = 2$ since $n = 2$.
Hence $2^4 = 4^2$ is the only solution.
Category:Equality of Integers to the Power of Each Other
Equality of Mappings

== Theorem ==
Two mappings $f_1: S_1 \to T_1, f_2: S_2 \to T_2$ are equal :
:$(1): \quad S_1 = S_2$
:$(2): \quad T_1 = T_2$
:$(3): \quad \forall x \in S_1: \map {f_1} x = \map {f_2} x$
== Proof ==
This follows directly from Equality of Relations.
== Also defined as ==
== Examples ==
== Sources ==
* : $\S 3.2$. Equality of mappings
* : $\S 2$: Sets and functions: Graphs and functions
* : $\S 4$. Relations; functional relations; mappings
* : $\S 20$: Introduction: Remarks $\text {(j)}$
* : Appendix $\text{A}.3$: Functions
Category:Mapping Theory
Category:Equality of Mappings
Equality of Mappings/Also defined as

== Equality of Mappings ==
It is worth labouring the point that for two mappings to be equal, not only must their domains be equal, but so must their codomains:
:It may seem like nit-picking to distinguish between functions which have different [ codomains but are otherwise equal] (and indeed until recently most authors did not) but failure to make the distinction sometimes leads to confusion.
::: -- 
:At first sight this may appear somewhat pedantic but we shall see later that not to do so can lead to confusion.
::: -- 
:This is a matter of convention. Some authors would say that $\theta$, $\phi$ are equal if $(1)$ [equality of domains] and $(3)$ [equality of images] hold, but this gives a little difficulty when defining the inverse mapping.
::: -- : $\S 3.2$. Equality of mappings (footnote)
Thus it is worth noting that this is a modern departure, and many earlier sources, for example , do not impose this condition, stating merely that two mappings are equal if the domains are equal and every element of the domain has the same image under each mapping.
Other sources, for example and , gloss over the topic, and merely assume equality of domains and codomains, implicitly stating the equality of the images.
, while careful to state equality of codomains, implicitly assumes that two mappings in question have the same domain to start with, and so misses a chance to explain the equality of the domains:
:... It also follows that two maps $f: X \to Y$ and $g: X \to Z$ can only be equal if $Y = Z$.
Earlier works, for example and tend to identify a mapping with its graph, preferring to dispense with a need to specify either its domain or its codomain.
== Sources ==
* : Introduction $\S 2$: Product sets, mappings
* : Chapter $0$: Functions
* : Chapter $\text {I}$: Elementary Definitions: $\S 3$. Homomorphisms
* : $\S 1.3$: Theorem $1.12$
* : $\S 2.2$: Functions: Exercise $\text{B} \ 1$
* : $\S 3.2$. Equality of mappings: Example $46$
* : Chapter $\text I$: Algebraic Structures: $\S 1$: The Language of Set Theory
* : Appendix: Elementary set and number theory
* : Chapter $1$: Mappings: $\S 10$
* : $\S 4$. Relations; functional relations; mappings: Remark $4$
* : Chapter $2$: Maps and relations on sets: Remark
* : $1$. Notation, Conventions: $10$
Category:Equality of Mappings
Equality of Mappings/Examples/Rotation of Plane 180 Degrees Clockwise and Anticlockwise

== Example of Equality of Mappings ==
Let $\Gamma$ denote the Cartesian plane.
Let $R_{180}: \Gamma \to \Gamma$ denote the rotation of $\Gamma$ about the origin anticlockwise through $180 \degrees$.
Let $R_{-180}: \Gamma \to \Gamma$ denote the rotation of $\Gamma$ about the origin clockwise through $180 \degrees$.
Then:
: $R_{180} = R_{-180}$
== Proof ==
The domains and codomains if both $R_{360}$ and $I_\Gamma$ are the same:
:$\Dom {R_{180} } = \Dom {R_{-180} } = \Gamma$
:$\Cdm {R_{180} } = \Cdm {R_{-180} } = \Gamma$
Then note that for all $\tuple {x, y}$:
:$R_{180} \tuple {x, y} = \tuple {-x, -y}$
and:
:$R_{-180} \tuple {x, y} = \tuple {-x, -y}$
The result follows by Equality of Mappings.
== Sources ==
* : Chapter $4$: Mappings: Exercise $2 \ \text {(ii)}$
Category:Examples of Equality of Mappings
Equality of Mappings/Examples/Rotation of Plane 360 Degrees equals Identity Mapping

== Example of Equality of Mappings ==
Let $\Gamma$ denote the Cartesian plane.
Let $R_{360}: \Gamma \to \Gamma$ denote the rotation of $\Gamma$ about the origin anticlockwise through $360 \degrees$.
Let $I_\Gamma: \Gamma \to \Gamma$ denote the identity mapping on $\Gamma$.
Then:
: $R_{360} = I_\Gamma$
== Proof ==
The domains and codomains if both $R_{360}$ and $I_\Gamma$ are the same:
:$\Dom {R_{360} } = \Dom {I_\Gamma} = \Gamma$
:$\Cdm {R_{360} } = \Cdm {I_\Gamma} = \Gamma$
Then note that for all $\tuple {x, y}$:
:$R_{360} \tuple {x, y} = \tuple {x, y}$
and:
:$I_\Gamma \tuple {x, y} = \tuple {x, y}$
The result follows by Equality of Mappings.
== Sources ==
* : Chapter $4$: Mappings: Exercise $2 \ \text {(i)}$
Category:Examples of Equality of Mappings
Equality of Mappings/Unequal/Examples/Exponential Functions

== Example of Mappings which are Unequal ==
Let $\theta: \R \to \R$ be the mapping from the set of real numbers to itself defined as:
:$\forall x \in \R: \map \theta x := e^x$
where $e^x$ denotes the real exponential function.
Let $\phi: \R \to \R_{>0}$ be the mapping from the set of real numbers to the set of (strictly) positive real numbers defined as:
:$\forall x \in \R: \map \phi x := e^x$
Then:
:$\phi \ne \theta$
because, while $\Dom \theta = \Dom \phi$, and $\forall x \in \R: \map \theta x = \map \phi x$, they have different codomains:
:$\Cdm \theta = \R \ne \R_{>0} = \Cdm \phi$
== Sources ==
* : $\S 3.2$. Equality of mappings: Example $46$
Category:Examples of Equality of Mappings
Equality of Monomials of Polynomial Ring in Multiple Variables

== Theorem ==
Let $R$ be a commutative ring with unity.
Let $I$ be a set.
Let $R \sqbrk {\sequence {x_i}_{i \mathop \in I} }$ be a polynomial ring in $I$ variables $\sequence {x_i}_{i \mathop \in I}$ over $R$.
Let $a, b : I \to \N$ be distinct mappings with finite support.
Then the monomials $\ds \prod_{i \mathop \in I} X_i^{a_i}$ and $\ds \prod_{i \mathop \in I} X_i^{b_i}$ are distinct, where:
:$X_i^k$ denotes the $k$th power of $X_i$
:$\prod$ denotes product with finite support 
== Proof ==
== Also see ==
* Equality of Monomials of Polynomial Ring
* Monomials of Polynomial Ring form Free Monoid
Category:Monomials
Equality of Monomials of Polynomial Ring in One Variable

== Theorem ==
Let $R$ be a commutative ring with unity.
Let $R \sqbrk X$ be a polynomial ring in one variable $X$ over $R$.
Let $k, l \in \N$ be distinct natural numbers.
Then the mononomials $X^k$ and $X^l$ are distinct, where $X^k$ denotes the $k$th power of $X$.
== Proof ==
By:
* Uniqueness of Polynomial Ring in One Variable
* Homomorphism Preserves Indexed Products
we may assume $R \sqbrk X$ is the ring of sequences of finite support over $R$, and $X$ is the sequence $\sequence {0, 1, 0, 0 \ldots}$.
One verifies that, for $k \ge 0$, $X^k$ is the sequence with $\map {X^k} l = \delta_{k l}$, where $\delta$ is the Kronecker delta.
Thus $X^k \ne X^l$ if $k \ne l$.
== Also see ==
* Equality of Monomials of Polynomial Ring
Category:Monomials
Equality of Natural Numbers

== Theorem ==
Let $m, n \in \N$.
Then:
:$\N_m \sim \N_n \iff m = n$
where $\sim$ denotes set equivalence and $\N_n$ denotes the set of all natural numbers less than $n$.
== Proof ==
By Set Equivalence behaves like Equivalence Relation, we have that:
:$m = n \implies \N_m \sim \N_n$
It remains to show that:
:$m \ne n \implies \N_m \nsim \N_n$.
Since the naturals are totally ordered, it will be sufficient to show that:
:$m \in \N_n \implies \N_m \nsim \N_n$
Let $S = \set {n \in \N: \forall m \in \N_n: \N_m \nsim \N_n}$.
That is, $S$ is the set of all the natural numbers $n$ such that $\N_m \nsim \N_n$ for all $m \in \N_n$.
We use mathematical induction to prove that $S = \N$.
From Initial Segment of Natural Numbers determined by Zero is Empty:
:$\N_0 = \O$
Thus $0 \in S$.
This is the basis for the induction.
Now, assume the induction hypothesis that $n \in S$.
We now complete the induction step, that is, to show that $n + 1 \in S$.
Let $m \in \N_{n + 1}$.
If $m = 0$, then $\N_m \nsim \N_{n + 1}$ because $\N_0 = \O$ and $\N_{n + 1} \ne \O$.
 that $m \ge 1$ and $\N_m \sim \N_{n + 1}$.
Then, by Set Equivalence Less One Element, that means $\N_{m - 1} \sim \N_n$.
But then $m - 1 \in \N_n$ which contradicts the induction hypothesis that $n \in S$.
Thus $n + 1 \in S$.
The result follows from the fact that Set Equivalence behaves like Equivalence Relation, in particular the symmetry clause.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 17$: Finite Sets: Theorem $17.3$
* : $\S 10.17$
Category:Natural Numbers
Category:Proofs by Induction
Equality of Open Balls does not imply Equality of Centers

== Theorem ==
Let $M = \struct {A, d}$ be a metric space.
Let $x, y \in A$ and $r, s \in \R$ such that:
:$\map {B_r} x = \map {B_s} y$
Then it is not necessarily the case that their centers $x$ and $y$ are equal.
== Proof ==
Let $A$ be arbitrary.
Let $d$ be the (standard) discrete metric on $A$.
Let $r \ge 1$ and $s \ge 1$.
Then from Open Ball in Standard Discrete Metric Space:
:$\forall x, y \in A: \map {B_r} x = \map {B_s} y = A$
whether $x = y$ or not.
== Sources ==
* : $2$: Continuity generalized: metric spaces: Exercise $2.6: 26$
Category:Open Balls
Equality of Open Balls does not imply Equality of Radii

== Theorem ==
Let $M = \struct {A, d}$ be a metric space.
Let $x, y \in A$ and $r, s \in \R$ such that:
:$\map {B_r} x = \map {B_s} y$
Then it is not necessarily the case that their radii $r$ and $s$ are equal.
== Proof ==
Let $A$ be arbitrary.
Let $d$ be the (standard) discrete metric on $A$.
Let $r \ge 1$ and $s \ge 1$ such that $r \ne s$.
Then from Open Ball in Standard Discrete Metric Space:
:$\forall x, y \in A: \map {B_r} x = \map {B_s} y = A$
== Sources ==
* : $2$: Continuity generalized: metric spaces: Exercise $2.6: 26$
Category:Open Balls
Equality of Ordered Pairs

== Theorem ==
Two ordered pairs are equal corresponding coordinates are equal:
:$\tuple {a, b} = \tuple {c, d} \iff a = c \land b = d$
== Proof ==
=== Necessary Condition ===
=== Sufficient Condition ===
== Also see ==
* Equality of Ordered Tuples
* Elements of Ordered Pair do not Commute, where it is formally noted that:
:$a \ne b \iff \tuple {a, b} \ne \tuple {b, a}$
that is:
:$\tuple {a, b} = \tuple {b, a} \iff a = b$
== Sources ==
* : Introduction $\S 2$: Product sets, mappings
* : Chapter $0$: Relations
* : $\S 1.7$. Pairs. Product of sets
* : Chapter $\text I$: Algebraic Structures: $\S 1$: The Language of Set Theory
* : $\S 0.2$. Sets
* : Introduction: Set-Theoretic Notation
* : Chapter $1$: The Notation and Terminology of Set Theory: $\S 9$
* : $\S 1.9$: Cartesian Product
* : $\S 1$: Naive Set Theory: $\S 1.4$: Sets of Sets: Exercise $1.4.1$
* 
* : Chapter $1$: Exercise $1.1$
* 
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 4$ The pairing axiom: Lemma $4.3$.
Category:Equality of Ordered Pairs
Category:Cartesian Product
Category:Axiomatic Set Theory
Category:Equality of Ordered Tuples
Category:Equality
Equality of Ordered Pairs/Lemma

== Theorem ==
Let $\set {a, b}$ and $\set {a, d}$ be doubletons such that $\set {a, b} = \set {a, d}$.
Then:
:$b = d$
== Proof ==
We have that:
:$b \in \set {a, b}$
and so by definition of set equality:
:$b \in \set {a, d}$
So:
:$(1): \quad$ either $b = a$ or $b = d$.
First suppose that $b = a$.
Then:
:$\set {a, b} = \set {a, a} = \set a$
We have that:
:$d \in \set {a, d}$
and so by definition of set equality:
:$d \in \set {a, b}$
and so as $\set {a, b} = \set a$ it follows that:
:$d = a$
We have $b = a$ and $d = a$, and so:
:$b = d$
Next suppose that $b \ne a$.
We have from $(1)$ that either $b = a$ or $b = d$.
As $b \ne a$ it must be the case that $b = d$.
So in either case we see that:
:$b = d$
== Sources ==
* : Exercise $1.1: \ 12$
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 4$ The pairing axiom: Lemma $4.3$.
Category:Equality of Ordered Pairs
Equality of Ordered Pairs/Necessary Condition

== Theorem ==
Let $\tuple {a, b}$ and $\tuple {c, d}$ be ordered pairs such that $\tuple {a, b} = \tuple {c, d}$.
Then $a = c$ and $b = d$.
== Proof from Kuratowski Formalization ==
== Proof from Empty Set Formalization ==
== Proof from Wiener Formalization ==
== Sources ==
* : $\S 6$: Ordered Pairs
* : Exercise $1.1: \ 12$
* : Exercise $1.11$
* : $\S 3$. Ordered pairs; cartesian product sets: Theorem $3.1$
* : $1$. Notation, Conventions: $9$: Theorem $1.3$
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 4$ The pairing axiom: Theorem $4.4$.
Category:Equality of Ordered Pairs
Equality of Ordered Pairs/Necessary Condition/Proof from Empty Set Formalization

== Theorem ==
== Proof ==
First a lemma:
Let $\tuple {a, b} = \tuple {c, d}$.
From the empty set formalization:
:$\set {\set {\O, a}, \set {\set \O, b} } = \set {\set {\O, c}, \set {\set \O, d} }$
First we note the special case where $a = \set \O$ and $b = \O$.
Then we have:
Thus we have that:
:$c = d = \set {\O, \set \O}$
and so:
:$c = \set \O$ and $d = \O$
leading to the result that $a = c$ and $b = d$.
Suppose otherwise, that either $a \ne \set \O$ or $b \ne \O$, or both.
Let $x \in \set {\set {\O, a}, \set {\set \O, b} }$.
Then either:
:$x = \set {\O, a}$
or:
:$x = \set {\set \O, b}$
First suppose $x = \set {\O, a}$.
Then:
:$x = \set {\O, c}$ or $x = \set {\set \O, d}$
 $x = \set {\set \O, d}$.
That is:
:$\set {\O, a} = \set {\set \O, d}$
which means that $a = \set \O$ and $d = \O$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\set \O, d}$.
Thus $x = \set {\O, c}$.
We have that:
:$x = \set {\O, a}$ and $x = \set {\O, c}$
and so:
:$\set {\O, a} = \set {\O, c}$
It follows from the lemma that:
:$a = c$
Now suppose $x = \set {\set \O, b}$.
Then:
:$x = \set {\O, c} \lor \set {\set \O, d}$
 $x = \set {\O, c}$.
That is:
:$\set {\set \O, b} = \set {\O, c}$
which means that $b = \O$ and $c = \set \O$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\O, c}$.
Thus $x = \set {\set \O, d}$.
We have that:
:$x = \set {\set \O, b}$ and $x = \set {\set \O, d}$
and so:
:$\set {\set \O, b} = \set {\set \O, d}$
It follows from the lemma that:
:$b = d$
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 4$ The pairing axiom: Exercise $4.1. \ \text{(a)}$
Category:Equality of Ordered Pairs