# prove two different forms of the same uniqueness theorem are logically equivalent

One may take either of the statements below as a definition of $(\exists!x)(P_x)$, where $P_x$ is a predicate concerning the set $x$.

Prove that they are logically equivalent.

$$(\exists x)(P_x) \land (\forall x)\bigl(P_x\implies(\forall y)(P_y\iff x=y)\bigr)\\ \dashv\vdash\\ (\exists x)(P_x) \land (\forall x)(\forall y)(P_x\land P_y \implies x=y)$$

# (in English)

"There exists a unique $x$ such that $P_x$ is true" may be defined as:

1. "There exists an $x$ for which $P$ is true, and for every $x$ for which $P$ is true, $P$ is true for another $y$ if and only if $x=y$."
2. "There exists an $x$ for which $P$ is true, and for any two $x$ and $y$ for which $P$ is true, then $x=y$."

# References

• Your formulae don’t match your prose. The prose version of no. 1 has just an implication $P_y \Rightarrow x = y$, where the first formula has an if-and-only-if, $P_y \Leftrightarrow x = y$. – Peter LeFanu Lumsdaine Dec 6 '13 at 22:21
• @PeterLeFanuLumsdaine: done. But let's be honest, we do have to acknowledge the fact that logical statements written in English are nowhere near as unambiguous as they are in Math. Don't even get me started on "and" vs. "or" :) – chharvey Dec 6 '13 at 22:24
• Everyday prose is often logically ambiguous. But carefully-written mathematical prose can be perfectly unambiguous; learning the conventions of clear mathematical writing is an important part of any mathematical education. – Peter LeFanu Lumsdaine Dec 6 '13 at 22:29

Hint 2. Now, take the two implications separately. Either way round, you’re trying to prove a universal statement, so the first thing to try is to assume any available hypotheses, and then to show the conclusion from them. For instance to show that version (1), $(\forall x)(P_x \Rightarrow (\forall y)(P_y \Leftrightarrow x = y))$, implies version (2), $(\forall x) (\forall y) (P_x \land P_y \Rightarrow x = y)$, first assume (1); then suppose given some $x$, and $y$, such that $P_x \land P_y$ holds; then from these assumptions, show that $x = y$. For the other direction, (2) $\Rightarrow$ (1), proceed similarly.