Singleton Equality

This page has been identified as a candidate for refactoring of basic complexity. In particular: Two results here. Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Theorems

Let $x$ and $y$ be sets.

Then:

$\set x \subseteq \set y \iff x = y$

$\set x = \set y \iff x = y$

Proof

\(\ds \)

\(\)

\(\ds \)

\(\ds \set x \subseteq \set y\)

\(\ds \)

\(\leadstoandfrom\)

\(\ds \forall z:\)

\(\ds \paren {z \in \set x \implies z \in \set y}\)

Definition of Subset

\(\ds \)

\(\leadstoandfrom\)

\(\ds \forall z:\)

\(\ds \paren {z = x \implies z = y}\)

Definition of Singleton

\(\ds \)

\(\leadstoandfrom\)

\(\ds \)

\(\ds x = y\)

Equality implies Substitution

$\Box$

Then:

\(\ds x\)

\(=\)

\(\ds y\)

\(\ds \leadsto \ \ \)

\(\ds \set x\)

\(=\)

\(\ds \set y\)

Substitutivity of Equality

\(\ds \leadsto \ \ \)

\(\ds \set x\)

\(\subseteq\)

\(\ds \set y\)

\(\ds \leadsto \ \ \)

\(\ds x\)

\(=\)

\(\ds y\)

by the first part

$\blacksquare$

Sources

• 1963: Willard Van Orman Quine: Set Theory and Its Logic: $\S 7.7$