Intersection With Singleton is Disjoint if Not Element

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $S$ be a set.

Let $\set x$ be the singleton of $x$.


Then:

$x \notin S$ if and only if $\set x \cap S = \O$


Proof

\(\displaystyle \) \(\) \(\displaystyle \set x \cap S = \O\)
\(\displaystyle \leadstoandfrom \ \ \) \(\displaystyle \) \(\) \(\displaystyle \forall y : \lnot \paren{ y \in \set x \cap S}\) Definition of Empty Set
\(\displaystyle \leadstoandfrom \ \ \) \(\displaystyle \) \(\) \(\displaystyle \forall y : \lnot \paren{ y \in \set x \land y \in S}\) Definition of Set Intersection
\(\displaystyle \leadstoandfrom \ \ \) \(\displaystyle \) \(\) \(\displaystyle \forall y : \lnot \paren{ y \in \set x \land \lnot \lnot \paren{y \in S} }\) Double Negation Introduction
\(\displaystyle \leadstoandfrom \ \ \) \(\displaystyle \) \(\) \(\displaystyle \forall y : y \in \set x \implies \lnot \paren{y \in S}\) Implication Equivalent to Negation of Conjunction with Negative
\(\displaystyle \leadstoandfrom \ \ \) \(\displaystyle \) \(\) \(\displaystyle \forall y : y \in \set x \implies y \notin S\) Definition of Not Element
\(\displaystyle \leadstoandfrom \ \ \) \(\displaystyle \) \(\) \(\displaystyle \forall y : y = x \implies y \notin S\) Definition of Singleton
\(\displaystyle \leadstoandfrom \ \ \) \(\displaystyle \) \(\) \(\displaystyle x \notin S\) Definition of Equality

$\blacksquare$