# Uniqueness Condition for Relation Value

## Theorem

Let $\mathcal R$ be a relation.

Let $\left({x, y}\right) \in \mathcal R$.

Let:

$\exists ! y: \left({x, y}\right) \in \mathcal R$

Then:

$\mathcal R \left({x}\right) = y$

where $\mathcal R \left({x}\right)$ denotes the image of $\mathcal R$ at $x$.

If $y$ is not unique, then:

$\mathcal R \left({x}\right) = \varnothing$

## Proof

 $(1):\quad$ $\displaystyle z \in \mathcal R \left({ x }\right)$ $\implies$ $\displaystyle \exists y: \left({z \in y \land \left({x, y}\right) \in \mathcal R }\right) \land \exists ! y: \left({x, y}\right) \in \mathcal R$ Definition of Image of Element under Relation $\displaystyle$ $\implies$ $\displaystyle \forall w: \left({\left({x, w}\right) \in \mathcal R \iff w = y}\right)$ Definition of Unique and by hypothesis that $\left({x, y}\right) \in \mathcal R$ $\displaystyle$ $\implies$ $\displaystyle \left({z \in w \land \left({x, w}\right) \in \mathcal R}\right)$ Existential Instantiation from $(1)$ $\displaystyle$ $\implies$ $\displaystyle z \in y$ Substitutivity of Equality from $z \in w \land w = y$

Conversely:

 $\displaystyle z \in y$ $\implies$ $\displaystyle \left({z \in y \land \left({x, y}\right) \in \mathcal R}\right)$ by hypothesis that $\left({x, y}\right) \in \mathcal R$ $\displaystyle$  $\displaystyle \exists ! y: \left({x, y}\right) \in \mathcal R$ by hypothesis $\displaystyle$ $\implies$ $\displaystyle z \in \mathcal R \left({x}\right)$ Definition of Image of Element under relation

Generalizing:

$\forall z: \left({z \in y \iff z \in \mathcal R \left({x}\right) }\right)$

Therefore:

$y = \mathcal R \left({x}\right)$

by the definition of class equality.

$\Box$

Suppose that $\neg \exists ! y: \left({x, y}\right) \in \mathcal R$.

Then:

 $\displaystyle \neg \exists ! y: \left({x, y}\right) \in \mathcal R$ $\implies$ $\displaystyle z \notin \mathcal R \left({x}\right)$ Definition of Image of Element under relation

Thus:

$\forall z: z \notin \mathcal R \left({ x }\right)$

Therefore:

$\mathcal R \left({ x }\right) = \varnothing$

$\blacksquare$