\begin{definition}[Definition:Precisely One Function]
Let $p_1, p_2, \ldots, p_n$ be statements.
The '''precisely one function''' is the propositional function $\map P {p_1, p_2, \ldots, p_n}$ defined as:
:$\map P {p_1, p_2, \ldots, p_n}$ is true {{iff}} '''precisely one''' of $p_1, p_2, \ldots, p_n$ is true.
{{help|It's got a name but I can't find it anywhere. I've seen it (we had something like this up on {{ProofWiki}} a decade ago but we must have deleted it for some reason). Anyone?}}
{{refactor|Put the below into its own page as a derived result}}
:$\exists p: p \in \set {p_1, p_2, \ldots, p_n}: \paren {p = \text {True} } \implies \forall x_1, x_2 \paren {x_1, x_2 \in \set {p_1, p_2, \ldots, p_n}: \paren {x_1 = \text {True} \land x_2 = \text {True} \implies \paren {x_1 = p} \land \paren {x_2 = p} } }$
\end{definition}