Intersection of Doubleton

From ProofWiki
Jump to navigation Jump to search


Let $x$ and $y$ be sets.

Let $\set {x, y}$ be a doubleton.

Then $\ds \bigcap \set {x, y}$ is a set such that:

$\ds \bigcap \set {x, y} = x \cap y$


\(\ds \) \(\) \(\ds z \in \bigcap \set {x, y}\)
\(\ds \leadstoandfrom \ \ \) \(\ds \) \(\) \(\ds \forall w \in \set {x, y}: z \in w\) Definition of Intersection of Class
\(\ds \leadstoandfrom \ \ \) \(\ds \) \(\) \(\ds \forall w: \paren {\paren {w = x \land w = y} \land z \in w}\) Definition of Doubleton Class
\(\ds \leadstoandfrom \ \ \) \(\ds \) \(\) \(\ds \paren {z \in x \land z \in y}\) Equality implies Substitution
\(\ds \leadstoandfrom \ \ \) \(\ds \) \(\) \(\ds z \in \paren {x \cap y}\) Definition of Class Intersection

From Intersection of Non-Empty Class is Set it follows that $x \cap y$ is a set.