Set Difference of Doubleton and Singleton is Singleton

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x, y$ be distinct objects.


Then:

$\set{x, y} \setminus \set x = \set y$


Proof

\(\ds \set{x, y} \setminus \set x\) \(=\) \(\ds \big \{ z: z \in \set{x, y} \land z \notin \set x \big \}\) Definition of Set Difference
\(\ds \) \(=\) \(\ds \big \{ z: \paren{ z = x \lor z = y} \land z \notin \set x \big \}\) Definition of Doubleton
\(\ds \) \(=\) \(\ds \big \{ z: \paren{ z = x \lor z = y} \land z \ne x \big \}\) Definition of Singleton
\(\ds \) \(=\) \(\ds \big \{ z: \paren{z = x \land z \ne x} \lor \paren {z = y \land z \ne x} \big \}\) Conjunction Distributes over Disjunction
\(\ds \) \(=\) \(\ds \big \{ z: \bot \lor \paren {z = y \land z \ne x} \big \}\) Definition of Contradiction
\(\ds \) \(=\) \(\ds \big \{ z: \paren {z = y \land z \ne x} \big \}\) Disjunction with Contradiction
\(\ds \) \(=\) \(\ds \big \{ z : z = y \big \}\) Rule of Simplification
\(\ds \) \(=\) \(\ds \set y\) Definition of Singleton

$\blacksquare$