avewright/proofwiki-math huggingface dataset:
Theorem: Set is Subset of Union

The union of two sets is a superset of each:
:$S \subseteq S \cup T$
:$T \subseteq S \cup T$

Proof:
Let $x \in S_\beta$ for some $\beta \in I$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S_\beta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \set {x: \exists \alpha \in I: x \in S_\alpha}
      | c = {{Defof|Indexed Family of Sets}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | l = S_\beta
      | o = \subseteq
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
As $\beta$ was arbitrary, it follows that:
:$\ds \forall \beta \in I: S_\beta \subseteq \bigcup_{\alpha \mathop \in I} S_\alpha$
{{qed}}
Theorem: Set is Subset of Union

The union of two sets is a superset of each:
:$S \subseteq S \cup T$
:$T \subseteq S \cup T$

Proof:
Let $\beta \in I$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \beta
      | o = \in
      | r = I
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \set \beta
      | o = \subseteq
      | r = I
      | c = Singleton of Element is Subset
}}
{{eqn | ll= \leadsto
      | l = \bigcup \set {S_\beta}
      | o = \subseteq
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = Union of Subset of Family is Subset of Union of Family
}}
{{eqn | ll= \leadsto
      | l = S_\beta
      | o = \subseteq
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = {{Defof|Set Union|subentry = Family of Sets}}
}}
{{end-eqn}}
So it follows that:
:$\ds \forall \beta \in I: S_\beta \subseteq \bigcup_{\alpha \mathop \in I} S_\alpha$
{{qed}}
Theorem: Set is Subset of Itself

Every set is a subset of itself:
:$\forall S: S \subseteq S$
Thus, by definition, the relation '''is a subset of''' is reflexive.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x
      | l = \leftparen {x \in S}
      | o = \implies
      | r = \rightparen {x \in S}
      | c = Law of Identity:
      | cc= a statement implies itself
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = S
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Subset of Set with Propositional Function

Let $S$ be a set.
Let $P: S \to \set {\T, \F}$ be a propositional function on $S$.
Then:
:$\set {x \in S: \map P x} \subseteq S$

Proof:
{{begin-eqn}}
{{eqn | l = s
      | o = \in
      | r = \set {x \in S: \map P x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = s
      | o = \in
      | r = \set {x \in S \land \map P x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = s
      | o = \in
      | r = \set {x \in S} \land \map P s
      | c = {{Defof|Set Definition by Predicate}}
}}
{{eqn | ll= \leadsto
      | l = s
      | o = \in
      | r = \set {x \in S}
      | c = Rule of Simplification
}}
{{eqn | ll= \leadsto
      | l = s
      | o = \in
      | r = S
      | c = {{Defof|Element}}
}}
{{eqn | ll= \leadsto
      | l = \set {x \in S: \map P x}
      | o = \subseteq
      | r = S
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Singleton of Element is Subset

Let $S$ be a set.
Let $\set x$ be the singleton of $x$.
Then:
:$x \in S \iff \set x \subseteq S$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \set x \subseteq A
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = \forall y: \paren {y \in \set x \implies y \in A}
      | c = {{Defof|Subset}}
}}
{{eqn | o = \leadstoandfrom
      | r = \forall y: \paren {y = x \implies y \in A}
      | c = {{Defof|Singleton}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A
      | c = Equality implies Substitution
}}
{{end-eqn}}
{{qed}}
Theorem: Singleton of Element is Subset

Let $S$ be a set.
Let $\set x$ be the singleton of $x$.
Then:
:$x \in S \iff \set x \subseteq S$

Proof:
=== Necessary Condition ===
Let $x \in S$.
We have:
:$\set x = \set {y \in S: y = x}$
From Subset of Set with Propositional Function:
:$\set {x \in S: \map P x} \subseteq S$
Hence:
:$\set x \subseteq S$
{{qed|lemma}}
=== Sufficient Condition ===
Let $\set x \subseteq S$.
From the definition of a subset:
:$x \in \set x \implies x \in S$
{{qed}}
Theorem: Subset Relation is Transitive

The subset relation is transitive:
:$\paren {R \subseteq S} \land \paren {S \subseteq T} \implies R \subseteq T$

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = \paren {R \subseteq S} \land \paren {S \subseteq T}
      | c =
}}
{{eqn | o = \leadsto
      | r = \paren {x \in R \implies x \in S} \land \paren {x \in S \implies x \in T}
      | c = {{Defof|Subset}}
}}
{{eqn | o = \leadsto
      | r = \paren {x \in R \implies x \in T}
      | c = Hypothetical Syllogism
}}
{{eqn | o = \leadsto
      | r = R \subseteq T
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Subset Relation is Transitive

The subset relation is transitive:
:$\paren {R \subseteq S} \land \paren {S \subseteq T} \implies R \subseteq T$

Proof:
Let $V$ be a basic universe.
By definition of basic universe, $R$, $S$ and $T$ are all elements of $V$.
By the {{axiom-link|Transitivity}}, $R$, $S$ and $T$ are all classes.
We are given that $R \subseteq S$ and $S \subseteq T$.
Hence by Subclass of Subclass is Subclass, $R$ is a subclass of $T$.
By Subclass of Set is Set, it follows that $R$ is a subset of $T$.
Hence the result.
{{qed}}
Theorem: Set Inequality

:$S \ne T \iff \paren {S \nsubseteq T} \lor \paren {T \nsubseteq S}$

Proof:
{{begin-eqn}}
{{eqn | l=S \ne T
      | o=\iff
      | r=\neg \paren {S = T}
      | c=
}}
{{eqn | o=\iff
      | r=\neg \paren {\paren {S \subseteq T} \land \paren {T \subseteq S} }
      | c={{Defof|Set Equality|index = 2}}
}}
{{eqn | o=\iff
      | r=\neg \paren {S \subseteq T} \lor \neg \paren {T \subseteq S}
      | c=De Morgan's Laws: Disjunction of Negations
}}
{{eqn | o=\iff
      | r=\paren {S \nsubseteq T} \lor \paren {T \nsubseteq S}
      | c=
}}
{{end-eqn}}
{{qed}}
Category:Set Theory
Category:Subsets
2ywb0aglxb8cep1v5bvlptji7213di3
Theorem: Set Equals Itself

All sets are equal to themselves:
:$\forall S: S = S$

Proof:
{{begin-eqn}}
{{eqn | l = S \subseteq S
      | o = \land 
      | r = S \supseteq S
      | c = Set is Subset of Itself
}}
{{eqn | ll= \leadsto
      | l = S
      | r = S
      | c = {{Defof|Set Equality}}
}}
{{end-eqn}}
{{qed}}
Category:Set Equality
0sgjaz6fxne0e6dc2vi4eh1wrgw4gsw
Theorem: Union is Smallest Superset

Let $S_1$ and $S_2$ be sets.
Then $S_1 \cup S_2$ is the smallest set containing both $S_1$ and $S_2$.
That is:
:$\paren {S_1 \subseteq T} \land \paren {S_2 \subseteq T} \iff \paren {S_1 \cup S_2} \subseteq T$

Proof:
=== Necessary Condition ===
From Union of Subsets is Subset:
:$\paren {S_1 \subseteq T} \land \paren {S_2 \subseteq T} \implies \paren {S_1 \cup S_2} \subseteq T$
{{qed|lemma}}
Theorem: Union with Empty Set

The union of any set with the empty set is the set itself:
:$S \cup \O = S$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = S
      | c = Set is Subset of Itself
}}
{{eqn | l = \O
      | o = \subseteq
      | r = S
      | c = Empty Set is Subset of All Sets
}}
{{eqn | ll= \leadsto
      | l = S \cup \O
      | o = \subseteq
      | r = S
      | c = Union is Smallest Superset
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = S \cup \O
      | c = Set is Subset of Union
}}
{{eqn | ll= \leadsto
      | l = S \cup \O
      | r = S
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Union with Empty Set

The union of any set with the empty set is the set itself:
:$S \cup \O = S$

Proof:
From Empty Set is Subset of All Sets:
:$\O \subseteq S$
From Union with Superset is Superset:
:$S \cup \O = S$
{{qed}}
Theorem: Intersection is Subset

The intersection of two sets is a subset of each:
:$S \cap T \subseteq S$
:$S \cap T \subseteq T$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \cap T
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = S \land x \in T
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = S
      | c = Rule of Simplification
}}
{{eqn | ll= \leadsto
      | l = S \cap T
      | o = \subseteq
      | r = S
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Similarly for $T$.
{{qed}}
Theorem: Intersection with Empty Set

The intersection of any set with the empty set is itself the empty set:
:$S \cap \O = \O$

Proof:
{{begin-eqn}}
{{eqn | l = S \cap \O
      | o = \subseteq
      | r = \O
      | c = Intersection is Subset
}}
{{eqn | l = \O
      | o = \subseteq
      | r = S \cap \O
      | c = Empty Set is Subset of All Sets
}}
{{eqn | ll= \leadsto
      | l = S \cap \O
      | r = \O
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection is Largest Subset

Let $T_1$ and $T_2$ be sets.
Then $T_1 \cap T_2$ is the largest set contained in both $T_1$ and $T_2$.
That is:
:$S \subseteq T_1 \land S \subseteq T_2 \iff S \subseteq T_1 \cap T_2$

Proof:
=== Sufficient Condition ===
From Set is Subset of Intersection of Supersets we have that:
:$S \subseteq T_1 \land S \subseteq T_2 \implies S \subseteq T_1 \cap T_2$
{{qed|lemma}}
Theorem: Intersection is Subset of Union

The intersection of two sets is a subset of their union:
:$S \cap T \subseteq S \cup T$

Proof:
{{begin-eqn}}
{{eqn | l = S \cap T
      | o = \subseteq
      | r = S
      | c = Intersection is Subset
}}
{{eqn | l = S
      | o = \subseteq 
      | r = S \cup T
      | c = Set is Subset of Union
}}
{{eqn | ll= \leadsto
      | l = S \cap T
      | o = \subseteq
      | r = S \cup T
      | c = Subset Relation is Transitive
}}
{{end-eqn}}
{{qed}}
Theorem: Union Distributes over Intersection

Set union is distributive over set intersection:
:$R \cup \paren {S \cap T} = \paren {R \cup S} \cap \paren {R \cup T}$

Proof:
=== Union Subset of Intersection ===
Let $\ds x \in S \cup \bigcap \mathbb T$.
We need to show that:
:$\ds x \in \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
and then by definition of subset we will have shown that:
:$\ds S \cup \bigcap \mathbb T \subseteq \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$.
So, we have that $\ds x \in S \cup \bigcap \mathbb T$.
By definition of set union, $x \in S$ or $\ds x \in \bigcap \mathbb T$.
So there are two cases to consider:
$(1): \quad$ Suppose $x \in S$.
Then by definition of set union, $\forall X \in \mathbb T: x \in S \cup X$.
So:
:$\ds x \in \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
$(2): \quad$ Suppose $\ds x \in \bigcap \mathbb T$.
Then by definition of set intersection:
:$\forall X \in \mathbb T: x \in X$
So by definition of set union:
:$\forall X \in \mathbb T: x \in S \cup X$
So:
:$\ds x \in \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
In both cases we see that:
:$\ds x \in \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
so by Proof by Cases, we have that:
:$\ds S \cup \bigcap \mathbb T \subseteq \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
{{qed|lemma}}
=== Intersection Subset of Union ===
Let $\ds x \in \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$.
We need to show that:
:$\ds x \in S \cup \bigcap \mathbb T$
and then by definition of subset we will have shown that:
:$\ds \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X} \subseteq S \cup \bigcap \mathbb T$.
So, we have that:
:$\ds x \in \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
By definition of set intersection:
:$(A): \quad \forall X \in \mathbb T: x \in S \cup X$
There are two cases to consider:
:$(1): \quad \forall X \in \mathbb T: x \in X$
Then  by definition of set intersection:
:$\ds x \in \bigcap_{X \mathop \in \mathbb T} X$
and so by definition of set union:
:$\ds x \in S \cup \bigcap \mathbb T$
:$(2): \quad \exists X \in \mathbb T: x \notin X$
From $(A)$ we have that $x \in S \cup X$.
But as $x \notin X$ it follows that $x \in S$.
Then by definition of set union:
:$\ds x \in S \cup \bigcap \mathbb T$
In both cases we see that:
:$\ds x \in S \cup \bigcap \mathbb T$
so by Proof by Cases, we have that:
:$\ds \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X} \subseteq S \cup \bigcap \mathbb T$
{{qed|lemma}}
So we have that:
:$S \cup \ds \bigcap \mathbb T \subseteq \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
and
:$\ds \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X} \subseteq S \cup \bigcap \mathbb T$
and so by definition of set equality:
:$S \cup \ds \bigcap \mathbb T = \bigcap_{X \mathop \in \mathbb T} \paren {S \cup X}$
{{qed}}
Theorem: Union Distributes over Intersection

Set union is distributive over set intersection:
:$R \cup \paren {S \cap T} = \paren {R \cup S} \cap \paren {R \cup T}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in R \cup \paren {S \cap T}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in R \lor \paren {x \in S \land x \in T}
      | c = {{Defof|Set Union}} and {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in R \lor x \in S} \land \paren {x \in R \lor x \in T}
      | c = Disjunction is Left Distributive over Conjunction
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {R \cup S} \cap \paren {R \cup T}
      | c = {{Defof|Set Union}} and {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Union Distributes over Intersection

Set union is distributive over set intersection:
:$R \cup \paren {S \cap T} = \paren {R \cup S} \cap \paren {R \cup T}$

Proof:
From Intersection Distributes over Union:
:$R \cap \paren {S \cup T} = \paren {R \cap S} \cup \paren {R \cap T}$
From the Duality Principle for Sets, exchanging $\cup$ for $\cap$ throughout, and vice versa, reveals the result:
:$R \cup \paren {S \cap T} = \paren {R \cup S} \cap \paren {R \cup T}$
{{qed}}
Theorem: Intersection Distributes over Union

Set intersection is distributive over set union:
:$R \cap \paren {S \cup T} = \paren {R \cap S} \cup \paren {R \cap T}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in R \cap \paren {S \cup T}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in R \land \paren {x \in S \lor x \in T}
      | c = {{Defof|Set Union}} and {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in R \land x \in S} \lor \paren {x \in R \land x \in T}
      | c = Conjunction is Left Distributive over Disjunction
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {R \cap S} \cup \paren {R \cap T}
      | c = {{Defof|Set Union}} and {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is Subset

:$S \setminus T \subseteq S$

Proof:
{{begin-eqn}}
{{eqn | l = x \in S \setminus T
      | o = \leadsto
      | r = x \in S \land x \notin T
      | c = {{Defof|Set Difference}}
}}
{{eqn | o = \leadsto
      | r = x \in S
      | c = Rule of Simplification
}}
{{end-eqn}}
The result follows from the definition of subset.
{{Qed}}
Theorem: Set Difference is Subset

:$S \setminus T \subseteq S$

Proof:
{{begin-eqn}}
{{eqn | l = S \setminus T
      | r = S \cap \complement_S \left({T}\right)
      | c = Set Difference as Intersection with Relative Complement
}}
{{eqn | o = \subseteq
      | r = S
      | c = Intersection is Subset
}}
{{end-eqn}}
{{Qed}}
Theorem: Set Difference with Empty Set is Self

The set difference between a set and the empty set is the set itself:
:$S \setminus \O = S$

Proof:
From Set Difference is Subset:
:$S \setminus \O \subseteq S$
From the definition of the empty set:
:$\forall x \in S: x \notin \O$
Let $x \in S$.
Thus:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = S \land x \notin \O
      | c = Rule of Conjunction
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = S \setminus \O
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = S \setminus \O
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Thus we have:
:$S \setminus \O \subseteq S$
and:
:$S \subseteq S \setminus \O$
So by definition of set equality:
:$S \setminus \O = S$
{{qed}}
Theorem: Set Difference with Self is Empty Set

The set difference of a set with itself is the empty set:
:$S \setminus S = \O$

Proof:
From Set is Subset of Itself:
:$S \subseteq S$
From Set Difference with Superset is Empty Set we have:
:$S \subseteq T \iff S \setminus T = \O$
Hence the result.
{{qed}}
Theorem: Set Difference Equals First Set iff Sets are Disjoint

:$S \setminus T = S \iff S \cap T = \O$

Proof:
Assume $S, T \subseteq \Bbb U$ where $\Bbb U$ is a universal set.
{{begin-eqn}}
{{eqn | l = S \setminus T
      | r = S
}}
{{eqn | ll= \leadstoandfrom
      | l = S \cap \map \complement T
      | r = S
      | c = Set Difference as Intersection with Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = S
      | o = \subseteq
      | r = \map \complement T
      | c = Intersection with Subset is Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = S \cap \map \complement {\map \complement T}
      | r = \O
      | c = Intersection with Complement is Empty iff Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = S \cap T
      | r = \O
      | c = Complement of Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Equal Set Differences iff Equal Intersections

:$R \setminus S = R \setminus T \iff R \cap S = R \cap T$

Proof:
{{begin-eqn}}
{{eqn | l = R \setminus S
      | r = R \setminus T
}}
{{eqn | ll= \leadstoandfrom
      | l = \set {x \in R: x \notin S}
      | r = \set {x \in R: x \notin T}
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall x \in R
      | l = x \notin S
      | o = \iff
      | r = x \notin T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall x \in R
      | l = x \in S
      | o = \iff
      | r = x \in T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \set {\paren {x \in R} \land \paren {x \in S} }
      | r = \set {\paren {x \in R} \land \paren {x \in T} }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = R \cap S
      | r = R \cap T
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Equal Set Differences iff Equal Intersections

:$R \setminus S = R \setminus T \iff R \cap S = R \cap T$

Proof:
From Set Difference and Intersection form Partition:
: $\paren {R \setminus S} \cup \paren {R \cap S} = R = \paren {R \setminus T} \cup \paren {R \cap T}$
: $\paren {R \cap S} \cap \paren {R \setminus S} = \O = \paren {R \cap T} \cap \paren {R \setminus T}$
whatever $R, S, T$ might be.
Let $R \setminus S = R \setminus T$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {\paren {R \setminus S} \cup \paren {R \cap S} } \setminus \paren {R \setminus S}
      | r = \paren {\paren {R \setminus T} \cup \paren {R \cap T} } \setminus \paren {R \setminus T}
}}
{{eqn | ll= \leadsto
      | l = \paren {R \cap S} \setminus \paren {R \setminus S}
      | r = \paren {R \cap T} \setminus \paren {R \setminus T}
      | c = Set Difference with Union is Set Difference
}}
{{end-eqn}}
Now, we have from Set Difference with Disjoint Set:
:$S \cap T = \O \iff S \setminus T = S$
and so:
:$\paren {R \cap S} \setminus \paren {R \setminus S} = R \cap S$
and:
:$\paren {R \cap T} \setminus \paren {R \setminus T} = R \cap T$
So:
:$R \cap S = R \cap T$
We can use exactly the same reasoning if we assume $R \cap S = R \cap T$:
{{begin-eqn}}
{{eqn | l = \paren {\paren {R \setminus S} \cup \paren {R \cap S} } \setminus \paren {R \cap S}
      | r = \paren {\paren {R \setminus T} \cup \paren {R \cap T} } \setminus \paren {R \cap T}
}}
{{eqn | ll= \leadsto
      | l = \paren {R \setminus S} \setminus \paren {R \cap S}
      | r = \paren {R \setminus T} \setminus \paren {R \cap T}
      | c = Set Difference with Union is Set Difference
}}
{{end-eqn}}
and then because of Set Difference with Disjoint Set as above:
:$\paren {R \setminus S} \setminus \paren {R \cap S} = R \setminus S$
and:
:$\paren {R \setminus T} \setminus \paren {R \cap T} = R \setminus T$
So:
:$R \setminus S = R \setminus T$
{{qed}}
Theorem: Euler's Number is Irrational

Euler's number $e$ is irrational.

Proof:
{{AimForCont}} that $e$ is rational.
Then there exist coprime integers $m$ and $n$ (and we can choose $n$ to be positive) such that:
:$\dfrac m n = e = \ds \sum_{i \mathop = 0}^\infty \frac 1 {i!}$ from the definition of Euler's number.
Multiplying both sides by $n!$, observe that:
:$\dfrac m n n! = n! \ds \sum_{i \mathop = 0}^\infty \frac 1 {i!} = \paren {\dfrac {n!} {0!} + \dfrac {n!} {1!} + \dfrac {n!} {2!} + \cdots + \dfrac {n!} {n!} } + \paren {\frac {n!} {\paren {n + 1}!} + \dfrac {n!} {\paren {n + 2}!} + \dfrac {n!} {\paren {n + 3}!} + \cdots}$
Hence:
{{begin-eqn}}
{{eqn | l = m \paren {n - 1}! - \paren {\frac {n!} {0!} + \frac {n!} {1!} + \frac {n!} {2!} + \cdots + \frac {n!} {n!} }
      | r = \frac 1 {\paren {n + 1} } + \frac 1 {\paren {n + 1} \paren {n + 2} } + \frac 1 {\paren {n + 1} \paren {n + 2} \paren {n + 3} } + \cdots
      | c = 
}}
{{eqn | o = <
      | r = \frac 1 {\paren {n + 1} } + \frac 1 {\paren {n + 1} \paren {n + 1} } + \frac 1 {\paren {n + 1} \paren {n + 1} \paren {n + 1} } + \cdots
      | c = 
}}
{{eqn | r = \sum_{i \mathop = 0}^\infty \paren {\frac 1 {n + 1} }^{\paren {i + 1} }
      | c = 
}}
{{eqn | r = \frac {\frac 1 {n + 1} } {1 - \frac 1 {n + 1} } = \frac 1 n \le 1\) from Sum of Infinite Geometric Sequence \(
      | c = 
}}
{{end-eqn}}
Observe that the quantity on the {{LHS}} must be an integer, as it is composed entirely of sums and differences of integer terms.
It must be strictly positive, as it is equal to:
:$\dfrac 1 {\paren {n + 1} } + \dfrac 1 {\paren {n + 1} \paren {n + 2} } + \dfrac 1 {\paren {n + 1} \paren {n + 2} \paren {n + 3} } + \cdots$
which is strictly positive.
Thus:
:$m \paren {n - 1}! - \paren {\dfrac {n!} {0!} + \dfrac {n!} {1!} + \dfrac {n!} {2!} + \cdots + \dfrac {n!} {n!} }$
must be a strictly positive integer less than $1$.
From this contradiction it follows that $e$ must be irrational.
{{qed}}
Theorem: Set Difference with Intersection

Let $S$ and $T$ be sets.

Proof:
Consider $R, S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universe.
Then:
{{begin-eqn}}
{{eqn | l = \paren {R \setminus S} \cap T
      | r = \paren {R \cap \map \complement S} \cap T
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {R \cap T} \cap \map \complement S
      | c = Intersection is Commutative and Intersection is Associative
}}
{{eqn | r = \paren {R \cap T} \setminus S
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference with Intersection

Let $S$ and $T$ be sets.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \paren {R \setminus S} \cap T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in R \land x \notin S} \land x \in T
      | c = {{Defof|Set Intersection}} and {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in R \land x \in T} \land x \notin S
      | c = Rule of Commutation and Rule of Association
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = x \in \paren {R \cap T} \setminus S
      | c = {{Defof|Set Intersection}} and {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}
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:
Suppose you were a member of a club with $n + 1$ members (including you).
Suppose it were time to elect a committee of $k$ members from that club.
From Cardinality of Set of Subsets, there are $\dbinom {n + 1} k$ ways to select the members to form this committee.
Now, you yourself may or may not be elected a member of this committee.
Suppose that, after the election, you are not a member of this committee.
Then, from Cardinality of Set of Subsets, there are $\dbinom n k$ ways to select the members to form such a committee.
Now suppose you ''are'' a member of the committee. Apart from you, there are $k - 1$ such members.
Again, from Cardinality of Set of Subsets, there are $\dbinom n {k - 1}$ ways of selecting the ''other'' $k - 1$ members so as to form such a committee.
In total, then, there are $\dbinom n k + \dbinom n {k - 1}$ possible committees.
Hence the result.
{{qed}}