# Intersection With Singleton is Disjoint if Not Element

## 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$