avewright/proofwiki-math huggingface dataset:
Theorem: Pascal's Rule

For positive integers $n, k$ with $1 \le k \le n$:
:$\dbinom n {k - 1} + \dbinom n k = \dbinom {n + 1} k$
This is also valid for the real number definition:
:$\forall r \in \R, k \in \Z: \dbinom r {k - 1} + \dbinom r k = \dbinom {r + 1} k$

Proof:
Let $n, k \in \N$ with $1 \le k \le n$.
{{begin-eqn}}
{{eqn | l = \binom n k + \binom n {k - 1}
      | r = \frac {n!} {k! \, \paren {n - k}!} + \frac {n!} {\paren {k - 1}! \, \paren {n - \paren {k - 1} }!}
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | r = \frac {n! \, \paren {n - \paren {k - 1} } } {k! \, \paren {n - k}! \, \paren {n - \paren {k - 1} } } + \frac {n! \, k} {\paren {k - 1}! \, \paren {n - \paren {k - 1} }! \ k}
      | c = multiplying by $1$
}}
{{eqn | r = \frac {n! \, \paren {n - k + 1} } {k! \, \paren {n - k + 1}!} + \frac {n! \, k} {k! \, \paren {n - k + 1}!}
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \frac {n! \, \paren {n - k + 1} + n! \, k} {k! \, \paren {n - k + 1}!}
      | c = Addition of Fractions
}}
{{eqn | r = \frac {n! \, \paren {n - k + 1 + k} } {k! \, \paren {n - k + 1}!}
      | c = 
}}
{{eqn | r = \frac {n! \, \paren {n + 1} } {k! \, \paren {n - k + 1}!}
      | c = 
}}
{{eqn | r = \frac {\paren {n + 1}!} {k! \, \paren {n + 1 - k}!}
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \binom {n + 1} k
      | c = {{Defof|Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference Union Intersection

:$S = \paren {S \setminus T} \cup \paren {S \cap T}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T} \cup \paren {S \cap T}
      | r = \paren {\paren {S \setminus T} \cup S} \cap \paren {\paren {S \setminus T} \cup T}
      | c = Union Distributes over Intersection
}}
{{eqn | r = S \cap \paren {\paren {S \setminus T} \cup T}
      | c = Set Difference Union First Set is First Set
}}
{{eqn | r = S \cap \paren {S \cup T}
      | c = Set Difference Union Second Set is Union
}}
{{eqn | r = S
      | c = Intersection Absorbs Union
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference Union Intersection

:$S = \paren {S \setminus T} \cup \paren {S \cap T}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T} \cup \paren {S \cap T}
      | r = S \setminus \paren {T \setminus T}
      | c = Set Difference with Set Difference is Union of Set Difference with Intersection
}}
{{eqn | r = S \setminus \O
      | c = Set Difference with Self is Empty Set
}}
{{eqn | r = S
      | c = Set Difference with Empty Set is Self
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference Union Intersection

:$S = \paren {S \setminus T} \cup \paren {S \cap T}$

Proof:
By Set Difference is Subset:
:$S \setminus T \subseteq S$
By Intersection is Subset:
:$S \cap T \subseteq S$
Hence from Union is Smallest Superset:
:$\paren {S \setminus T} \cup \paren {S \cap T} \subseteq S$
Let $s \in S$.
Either:
:$s \in T$, in which case $s \in S \cap T$ by definition of set intersection
or
:$s \notin T$, in which case $s \in S \setminus T$ by definition of set difference.
That is, by definition of set union:
:$s \in \paren {S \setminus T} \cup \paren {S \cap T}$
and so by definition of subset:
:$S \subseteq \paren {S \setminus T} \cup \paren {S \cap T}$
Hence the result by definition of set equality.
{{qed}}
Theorem: Absorption Laws (Logic)

For any two propositions $p$ and $q$, we have:

Proof:
By calculation:
{{begin-eqn}}
{{eqn | l = p \land \paren {p \lor q}
      | r = \paren {p \lor \bot} \land \paren {p \lor q}
      | c = Disjunction with Contradiction
}}
{{eqn | r = p \lor \paren {\bot \land q}
      | c = Disjunction is Left Distributive over Conjunction
}}
{{eqn | r = p \lor \bot
      | c = Conjunction with Contradiction
}}
{{eqn | r = p
      | c = Disjunction with Contradiction
}}
{{end-eqn}}
{{qed}}
Theorem: Absorption Laws (Logic)

For any two propositions $p$ and $q$, we have:

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the appropriate truth values match for all boolean interpretations.
$\begin{array}{|ccccc||c|} \hline
p & \land & (p & \lor & q) & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \F & \F & \T & \T & \F \\
\T & \T & \T & \T & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Absorption Laws (Logic)

For any two propositions $p$ and $q$, we have:

Proof:
{{begin-eqn}}
{{eqn | l = p \lor \paren {p \land q}
      | r = \paren {p \land \top} \lor \paren {p \land q}
      | c = Conjunction with Tautology
}}
{{eqn | r = p \land \paren {\top \lor q}
      | c = Conjunction is Left Distributive over Disjunction
}}
{{eqn | r = p \land \top
      | c = Disjunction with Tautology
}}
{{eqn | r = p
      | c = Conjunction with Tautology
}}
{{end-eqn}}
{{qed}}
Theorem: Absorption Laws (Logic)

For any two propositions $p$ and $q$, we have:

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the appropriate truth values match for all boolean interpretations.
$\begin{array}{|ccccc||c|} \hline
p & \lor & (p & \land & q) & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F \\
\T & \T & \T & \F & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Set Difference with Set Difference

:$S \setminus \paren {S \setminus T} = S \cap T = T \setminus \paren {T \setminus S}$

Proof:
From the {{axiom-link|Transitivity}}, all sets are classes.
The result then follows from Class Difference with Class Difference.
{{finish|Find the result that demonstrate the set difference of two sets is also a set, intersection as well. Probably via subset of set is set or something.}}
Theorem: Set Difference is Anticommutative

Set difference is an anticommutative operation:
:$S = T \iff S \setminus T = T \setminus S = \O$

Proof:
From Set Difference with Superset is Empty Set we have:
:$S \subseteq T \iff S \setminus T = \O$
:$T \subseteq S \iff T \setminus S = \O$
The result follows from definition of set equality:
:$S = T \iff \paren {S \subseteq T} \land \paren {T \subseteq S}$
{{qed}}
Theorem: Dirichlet's Test for Uniform Convergence

Let $D$ be a set.
Let $\struct {V, \norm {\,\cdot\,} }$ be a normed vector space.
Let $a_i, b_i$ be mappings from $D \to M$.
{{explain|What is $M$? Should be $V$?}}
Let the following conditions be satisfied:
:$(1): \quad$ The sequence of partial sums of $\ds \sum_{n \mathop = 1}^\infty \map {a_n} x$ be bounded on $D$
:$(2): \quad \sequence {\map {b_n} x}$ be monotonic for each $x \in D$
{{explain|But $V$ is not ordered. Need to assume $V{{=}}\R$?}}
:$(3): \quad \map {b_n} x \to 0$ converge uniformly on $D$.
Then:
:$\ds \sum_{n \mathop = 1}^\infty \map {a_n} x \map {b_n} x$ converges uniformly on $D$.

Proof:
Suppose $\map {b_n} x \ge \map {b_{n + 1} } x$ for each $x \in D$.
All we need to show is that:
:$\ds \sum_{n \mathop = 1}^\infty \size {\map {b_n} x - \map {b_{n + 1} } x}$
converges uniformly on $D$.
{{explain|Why is the above sufficient? On the surface of it, no reference has been made to $\map {a_n} x$. Its connection to the above statement needs to be clarified.}}
To do this we show that the Cauchy criterion holds.
Assign $\epsilon < 0$.
Then by definition of uniform convergence:
:$\exists N \in \N: \forall x \in D: \forall n \ge N: \size {\map {b_n} x} < \dfrac \epsilon 2$
Let $x \in D$ and $n > m \ge N$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = m + 1}^n \size {\map {b_k} x - \map {b_{k + 1} } x}
      | r = \sum_{k \mathop = m + 1}^n \paren {\map {b_k} x - \map {b_{k + 1} } x}
}}
{{eqn | r = \map {b_{m + 1} } x - \map {b_{n + 1} } x
}}
{{eqn | r = \size {\map {b_{m + 1} } x - \map {b_{n + 1} } x}
}}
{{eqn | o = \le
      | r = \size {\map {b_{m + 1} } x + \map {b_{n + 1} } x}
}}
{{eqn | o = <
      | r = \frac \epsilon 2 + \frac \epsilon 2
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
{{qed}}
Theorem: Relative Complement of Empty Set

The relative complement of the empty set is the set itself:
:$\relcomp S \O = S$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp S \O
      | r = S \setminus \O
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = S
      | c = Set Difference with Empty Set is Self
}}
{{end-eqn}}
{{qed}}
Theorem: Relative Complement with Self is Empty Set

The relative complement of a set in itself is the empty set:
:$\relcomp S S = \O$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp S S
      | r = S \setminus S
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \O
      | c = Set Difference with Self is Empty Set
}}
{{end-eqn}}
{{qed}}
Theorem: Relative Complement of Relative Complement

:$\relcomp S {\relcomp S T} = T$

Proof:
By the definition of relative complement:
:$\relcomp S {\relcomp S T} = S \setminus \paren {S \setminus T}$
Let $t \in T$.
Then by the definition of set difference:
:$t \notin S \setminus T$
Since $t \in T$ and $T \subseteq S$, by the definition of subset:
:$t \in S$
Thus:
:$t \in \paren {S \setminus \paren {S \setminus T} }$
Suppose instead that:
:$t \in \paren {S \setminus \paren {S \setminus T} }$
Then:
:$t \in S$
and:
:$\neg \paren {t \in \paren {S \setminus T} }$
Thus:
:$\neg \paren {\paren {t \in S} \land \neg \paren {t \in T} }$
By Conditional is Equivalent to Negation of Conjunction with Negative:
:$t \in S \implies t \in T$
By Modus Ponendo Ponens:
:$t \in T$
{{qed}}
Theorem: Relative Complement of Relative Complement

:$\relcomp S {\relcomp S T} = T$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp S {\relcomp S T}
      | r = S \setminus \paren {S \setminus T}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = S \cap T
      | c = Set Difference with Set Difference
}}
{{end-eqn}}
The definition of the relative complement requires that:
:$T \subseteq S$
But from Intersection with Subset is Subset:
:$T \subseteq S \iff T \cap S = T$
Thus:
:$\relcomp S {\relcomp S T} = T$
follows directly.
{{qed}}
Theorem: Intersection with Relative Complement is Empty

The intersection of a set and its relative complement is the empty set:
:$T \cap \relcomp S T = \O$

Proof:
{{begin-eqn}}
{{eqn | l = T \cap \relcomp S T
      | r = \paren {S \setminus T} \cap T
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \O
      | c = Set Difference Intersection with Second Set is Empty Set
}}
{{end-eqn}}
{{qed}}
Theorem: Union with Relative Complement

The union of a set $T$ and its relative complement in $S$ is the set $S$:
:$\relcomp S T \cup T = S$

Proof:
=== Step 1 ===
By the definition of relative complement, we have that:
:$\relcomp S T \subseteq S$
and:
:$T \subseteq S$
Hence by Union is Smallest Superset:
:$\relcomp S T \cup T\subseteq S$
{{qed|lemma}}
Theorem: Set Difference as Intersection with Relative Complement

Let $A, B \subseteq S$.
Then the set difference between $A$ and $B$ can be expressed as the intersection with the relative complement with respect to $S$:
:$A \setminus B = A \cap \relcomp S B$

Proof:
{{begin-eqn}}
{{eqn | l = A \setminus B
      | r = \set {x: x \in A \land x \notin B}
      | c = {{Defof|Set Difference}}
}}
{{eqn | r = \set {x: \paren {x \in A \land x \in X} \land x \notin B}
      | c = {{Defof|Subset}}, Modus Ponens and Rule of Conjunction
}}
{{eqn | r = \set {x: x \in A \land \paren {x \in X \land x \notin B} }
      | c = Conjunction is Associative
}}
{{eqn | r = \set {x: x \in A \land x \in \relcomp S B}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = A \cap \relcomp S B
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Axiom Schemata for Groups

In the definition of a group, the axioms for the existence of an identity element and for closure under taking inverses can be replaced by the following two axioms:
:Given a group $G$, there exists at least one element $e \in G$ such that $e$ is a '''left identity''';
:For any element $g$ in a group $G$, there exists at least one '''left inverse''' of $g$.
Alternatively, we can also replace the aforementioned axioms with the following two:
:Given a group $G$, there exists at least one element $e \in G$ such that $e$ is a '''right identity''';
:For any element $g$ in a group $G$, there exists at least one '''right inverse''' of $g$.
Thus we can formulate the group axioms as either of the following:

Proof:
Suppose we define a group $G$ in the usual way, but make the first pair of axiom replacements listed above:
:the existence of a left identity
:every element has a left inverse.
Let $e \in G$ be a left identity and $g \in G$.
Then, from Left Inverse for All is Right Inverse, each left inverse is also a right inverse with respect to the left identity.
Also from Left Identity while exists Left Inverse for All is Identity we have that the left identity is also a right identity.
Also we have that such an Identity is Unique, so this element can rightly be called '''the''' identity.
So we have that:
:$G$ has an identity;
:each element of $G$ has an element that is both a left inverse and a right inverse with respect to this identity.
Therefore, the validity of the two axiom replacements is proved.
{{qed}}
The proof of the alternate pair of replacements (existence of a right identity and closure under taking right inverses) is similar.
Theorem: Group has Latin Square Property

Let $\struct {G, \circ}$ be a group.
Then $G$ satisfies the Latin square property.
That is, for all $a, b \in G$, there exists a unique $g \in G$ such that $a \circ g = b$.
Similarly, there exists a unique $h \in G$ such that $h \circ a = b$.

Proof:
Follows directly from the definition of both a Cayley table and a Latin square.
Theorem: Group has Latin Square Property

Let $\struct {G, \circ}$ be a group.
Then $G$ satisfies the Latin square property.
That is, for all $a, b \in G$, there exists a unique $g \in G$ such that $a \circ g = b$.
Similarly, there exists a unique $h \in G$ such that $h \circ a = b$.

Proof:
Let $G$ be a finite group whose order is $n$.
Let $\tuple {x_1, x_2, \ldots, x_n}$ be the elements of the underlying set of $G$ in the order they appear in the headings of the Cayley table of $G$.
Consider the row of the Cayley table headed with $a$.
The elements of that row are:
:$\tuple {a x_1, a x_2, \ldots, a x_n}$
that is:
:$\tuple {\map {\lambda_a} {x_1}, \map {\lambda_a} {x_2}, \ldots, \map {\lambda_a} {x_n} }$
where $\lambda_a$ denotes the left regular representation of $\struct {S, \circ}$ with respect to $a$.
From Regular Representations in Group are Permutations, it follows that each of $\map {\lambda_a} {x_1}, \map {\lambda_a} {x_2}, \ldots, \map {\lambda_a} {x_n}$ appears in that row exactly once.
A similar argument based on the right regular representation proves the result for the columns.
{{qed}}
Theorem: Group has Latin Square Property

Let $\struct {G, \circ}$ be a group.
Then $G$ satisfies the Latin square property.
That is, for all $a, b \in G$, there exists a unique $g \in G$ such that $a \circ g = b$.
Similarly, there exists a unique $h \in G$ such that $h \circ a = b$.

Proof:
{{begin-eqn}}
{{eqn | l = g
      | r = a^{-1} \circ b
}}
{{eqn | ll= \leadsto
      | l = a \circ g
      | r = a \circ \paren {a^{-1} \circ b}
}}
{{eqn | ll= \leadsto
      | l = a \circ g
      | r = \paren {a \circ a^{-1} } \circ b
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = a \circ g
      | r = e \circ b
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = a \circ g
      | r = b
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
Thus, such a $g$ exists.
Suppose $g, g' \in G$ where $a \circ g = b = a \circ g'$.
Then:
{{begin-eqn}}
{{eqn | l = g
      | r = e \circ g
      | c = {{Group-axiom|2}}
}}
{{eqn | r = \paren {a^{-1} \circ a} \circ g
      | c = {{Group-axiom|3}}
}}
{{eqn | r = a^{-1} \circ \paren {a \circ g}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = a^{-1} \circ b
      | c = Substitution for $a \circ g$
}}
{{eqn | r = a^{-1} \circ \paren {a \circ g'}
      | c = Substitution for $a \circ g'$
}}
{{eqn | r = \paren {a^{-1} \circ a} \circ g'
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e \circ g'
      | c = {{Group-axiom|3}}
}}
{{eqn | r = g'
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
Thus uniqueness holds.
To prove the second part of the theorem, let $h = b \circ a^{-1}$.
The remainder of the proof follows a similar procedure to the above.
{{qed}}
Theorem: Group has Latin Square Property

Let $\struct {G, \circ}$ be a group.
Then $G$ satisfies the Latin square property.
That is, for all $a, b \in G$, there exists a unique $g \in G$ such that $a \circ g = b$.
Similarly, there exists a unique $h \in G$ such that $h \circ a = b$.

Proof:
We shall prove that this is true for the first equation:
{{begin-eqn}}
{{eqn | l = a \circ g
      | r = b
}}
{{eqn | ll= \leadstoandfrom
      | l = a^{-1} \circ \paren {a \circ g}
      | r = a^{-1} \circ b
      | c = $\circ$ is a Cancellable Binary Operation
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {a^{-1} \circ a} \circ g
      | r = a^{-1} \circ b
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = e \circ g
      | r = a^{-1} \circ b
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadstoandfrom
      | l = g
      | r = a^{-1} \circ b
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
Because the statements:
:$a \circ g = b$
and
:$g = a^{-1} \circ b$
are equivalent, we may conclude that $g$ is indeed the only solution of the equation.
The proof that the unique solution of $h$ is $b \circ a^{-1}$ in the second equation follows similarly.
{{qed}}
Theorem: Group has Latin Square Property

Let $\struct {G, \circ}$ be a group.
Then $G$ satisfies the Latin square property.
That is, for all $a, b \in G$, there exists a unique $g \in G$ such that $a \circ g = b$.
Similarly, there exists a unique $h \in G$ such that $h \circ a = b$.

Proof:
Suppose that $\exists x, y \in G: a \circ x = b = a \circ y$.
{{begin-eqn}}
{{eqn | l = a \circ x
      | r = a \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a^{-1} \circ \paren {a \circ x}
      | r = a^{-1} \circ \paren {a \circ y}
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = \paren {a^{-1} \circ a} \circ x
      | r = \paren {a^{-1} \circ a} \circ y
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = e \circ x
      | r = e \circ y
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
So such an element, if it exists, is unique.
Now it is demonstrated that $g = a^{-1} b$ satisfies the requirement for $a \circ g = b$
Since $a \in G$, it follows by group axiom $G3$: existence of inverses that $a^{-1} \in G$.
{{begin-eqn}}
{{eqn | l = a
      | o = \in
      | r = G
}}
{{eqn | ll= \leadsto
      | l = a^{-1}
      | o = \in
      | r = G
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = a^{-1} \circ b
      | o = \in
      | r = G
      | c = {{Group-axiom|0}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = a \circ g
      | r = a \circ \paren {a^{-1} \circ b}
}}
{{eqn | r = \paren {a \circ a^{-1} } \circ b
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e \circ b
      | c = {{Group-axiom|3}}
}}
{{eqn | r = b
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
Thus, such a $g$ exists.
The properties of $h$ are proved similarly.
{{qed}}
Theorem: Group has Latin Square Property

Let $\struct {G, \circ}$ be a group.
Then $G$ satisfies the Latin square property.
That is, for all $a, b \in G$, there exists a unique $g \in G$ such that $a \circ g = b$.
Similarly, there exists a unique $h \in G$ such that $h \circ a = b$.

Proof:
We shall prove that this is true for the first equation:
{{begin-eqn}}
{{eqn | l = b
      | r = a \circ g
}}
{{eqn | ll= \leadsto
      | l = a^{-1} \circ b
      | r = a^{-1} \circ \paren {a \circ g}
      | c = {{Group-axiom|3}}
}}
{{eqn | r = \paren {a^{-1} \circ a} \circ g
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e \circ g
      | c = {{Group-axiom|3}}
}}
{{eqn | r = g
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
Conversely:
{{begin-eqn}}
{{eqn | l = g
      | r = a^{-1} \circ b
}}
{{eqn | ll= \leadsto
      | l = a \circ g
      | r = a \circ \paren {a^{-1} \circ b}
      | c = 
}}
{{eqn | r = \paren {a \circ a^{-1} } \circ b
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e \circ b
      | c = {{Group-axiom|3}}
}}
{{eqn | r = b
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
The proof that the unique solution of $h$ is $b \circ a^{-1}$ in the second equation follows similarly.
{{qed}}
Theorem: Symmetric Difference is Commutative

Symmetric difference is commutative:
:$S \symdif T = T \symdif S$

Proof:
{{begin-eqn}}
{{eqn | l = S \symdif T
      | r = \paren {S \setminus T} \cup \paren {T \setminus S}
      | c = {{Defof|Symmetric Difference}}
}}
{{eqn | r = \paren {T \setminus S} \cup \paren {S \setminus T}
      | c = Union is Commutative
}}
{{eqn | r = T \symdif S
      | c = {{Defof|Symmetric Difference}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Equivalence of Definitions of Symmetric Difference

Let $S$ and $T$ be sets.
{{TFAE|def = Symmetric Difference|view = symmetric difference $S \symdif T$ between $S$ and $T$}}
=== Definition 1 ===
{{:Definition:Symmetric Difference/Definition 1}}
=== Definition 2 ===
{{:Definition:Symmetric Difference/Definition 2}}
=== Definition 3 ===
{{:Definition:Symmetric Difference/Definition 3}}
=== Definition 4 ===
{{:Definition:Symmetric Difference/Definition 4}}
=== Definition 5 ===
{{:Definition:Symmetric Difference/Definition 5}}

Proof:
=== $(1)$ iff $(2)$ ===
{{:Equivalence of Definitions of Symmetric Difference/(1) iff (2)}}
{{qed|lemma}}
Theorem: Symmetric Difference of Equal Sets

The symmetric difference of two equal sets is the empty set:
:$S = T \iff S \symdif T = \O$

Proof:
{{begin-eqn}}
{{eqn | l = S = T
      | o = \leadstoandfrom
      | r = S \subseteq T \land T \subseteq S
      | c = {{Defof|Set Equality}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {S \setminus T = \O} \land \paren {T \setminus S = \O}
      | c = Set Difference with Superset is Empty Set
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {S \setminus T} \cup \paren {T \setminus S} = \O
      | c = Union is Empty iff Sets are Empty
}}
{{eqn | o = \leadstoandfrom
      | r = S \symdif T = \O
      | c = {{Defof|Symmetric Difference}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Union is Empty iff Sets are Empty

If the union of two sets is the empty set, then both are themselves empty:
:$S \cup T = \O \iff S = \O \land T = \O$

Proof:
{{begin-eqn}}
{{eqn | r = S \cup T = \O
      | o = 
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \neg \exists x
      | r = x \in \paren {S \cup T}
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \forall x
      | r = \neg \paren {x \in \paren {S \cup T} }
      | c = De Morgan's Laws (Predicate Logic)
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \forall x
      | r = \neg \paren {x \in S \lor x \in T}
      | c = {{Defof|Set Union}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \forall x
      | r = x \notin S \land x \notin T
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = S = \O \land T = \O
      | c = {{Defof|Empty Set}}
}}
{{end-eqn}}
{{qed}}
Theorem: Union is Empty iff Sets are Empty

If the union of two sets is the empty set, then both are themselves empty:
:$S \cup T = \O \iff S = \O \land T = \O$

Proof:
Let $S \cup T = \O$.
We have:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = S \cup T
      | c = Set is Subset of Union
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = \O
      | c = {{hypothesis}}
}}
{{end-eqn}}
From Empty Set is Subset of All Sets:
:$\O \subseteq S$
So it follows by definition of set equality that $S = \O$.
Similarly for $T$.
{{qed}}
Theorem: Symmetric Difference with Empty Set

:$S \symdif \O = S$
where $\symdif$ denotes the symmetric difference.

Proof:
{{begin-eqn}}
{{eqn | l = S \symdif \O
      | r = \paren {S \cup \O} \setminus \paren {S \cap \O}
      | c = {{Defof|Symmetric Difference|index = 2}}
}}
{{eqn | r = S \setminus \paren {S \cap \O}
      | c = Union with Empty Set
}}
{{eqn | r = S \setminus \O
      | c = Intersection with Empty Set
}}
{{eqn | r = S
      | c = Set Difference with Empty Set is Self
}}
{{end-eqn}}
{{qed}}