existence equivalence proofs Confused about proving equivalence for 
∃!x, p(x) and [∃x, p(x)] ∧ [∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z)]
I thought about using <=>, and using a verbal argument:
(=>) If x is unique and exists such that p(x) is true, then (∃x, p(x)) is implied, and if p(x) is ever true, it must be that if some other variable m fits p(m), m will equal x. That is implied by ∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z). In both scenarios, x is stated to be unique and existing. 
Is that legitimate?
 A: First, careful with the parentheses! It should be:
[∃x, p(x) ∧ [∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z)]]
Second, your verbal argument is a bit of a strange mix-up of both the $\Rightarrow$ direction as well as the $\Leftarrow$ direction that you need to show. For example, by saying that:

If x is unique ...

you clearly start out by going in the $\Rightarrow$ direction, but when you say:

... it must be that if some other variable m fits p(m), m will equal x. That is implied by ∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z).

you are suddenly going in the $\Leftarrow$ direction.  Indeed, I think you manage to confuse yourself: you indicate that you are going to try to show:

(=>) 

but in the end you say:

In both scenarios, ...

as if you have somehow shown both directions.
And in the end, I would say you have shown neither direction in a satisfactory way. In particular, for the $\Rightarrow$ direction, you have not shown that ∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z).  And for the $\Leftarrow$ direction, I would say that you need to flesh out the 

.. That is implied by ∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z).

A: (=>)
If there exists a unique x such that p(x) is true, ∃x, p(x) is already implied. Suppose that for all y, and for all z, fix y and z that p(y) and p(z) holds. If there is a unique / only one parameter that p(x) is true, then x = y = z, which implies y = z, otherwise x is not unique, which is a contradiction. Hence ∃!x, p(x) =>  [∃x, p(x) ∧ [∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z)]. 
(<=)
If [∃x, p(x) ∧ [∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z)], then ∃x, p(x) is already implied. Suppose that for all m, fix m that p(m) is true. Then 
∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z) implies that x must equal m, since both p(m) and p(x) are true. That means there is only one value of x that can suffice for p(x), in other words uniqueness. Hence [∃x, p(x) ∧ [∀y, ∀z, (p(y) ∧ p(z) ⇒ y = z)] => ∃!x, p(x).
As I have shown that both statements are implied by one another, they are equivalent. QED
