"$\forall x$ s.t. $\phi(x), \exists y$ s.t $\phi'(x,y)$" versus "$\forall x, \big( \phi(x)\implies \exists y $ s.t $\phi'(x,y)\big)$" I am trying to gain some insight into how one understands proofs that can be generically described as fitting this mold:

Let $x$ be some object that has a specific list of properties. Show that some other object $y$ exists with a specific property that relates to $x$. 

(An example of such a proof that follows this form can be found here: Proof of a proposition about recursion definition (Terence Tao's Analysis I)).
To tackle such a proof, I would do the following:
Firstly, I would note that this statement can be formally restated as:
$$\forall x \text{ such that } \phi(x), \exists y \text { such that } \phi'(x,y)$$
Then, I would pick an arbitrary element $x^*$ that satisfies $\phi(x^*)$. From this, I would try to construct a corresponding $y^*$ that satisfies $\phi'(x^*,y^*)$.
Because $x^*$ was arbitrary, I have thus proven that "$\forall x \text{ such that } \phi(x), \exists y \text { such that } \phi'(x,y)$" is a true statement. 
I believe this is the standard strategy.

I have always wondered how (and if) the aforementioned strategy can be reformulated using implications. An author of an "Answer Post" from a question posed here (Conceptual question about assuming the existence of a function in order to prove the existence of another function) made the following (paraphrased) comment:

The "such that $\phi(x)$" statement can actually be reformulated as an antecedent of an implication. Additionally, the "$\exists y \text{ such that } \phi'(x,y)$" can be reformulated as the consequent of the same implication. Therefore, "$\forall x \text{ such that } \phi(x), \exists y \text { such that } \phi'(x,y)$" is actually logically equivalent to "$\forall x, \big( \phi(x)\implies \exists y \text { such that } \phi'(x,y)\big) $."

Could some please elaborate on this a little more?
Edit: The proper format may actually be "$\forall x, \exists y \big( \phi(x)\implies \phi'(x,y)\big) $"
(however I am not sure)
 A: The exact same strategy works for the reformulated statement, since they're equivalent.  If you want to prove $$\forall x(\phi(x)\implies \exists y,\phi'(xy))$$  what do you do?  Pick an arbitrary $x$ such that $\phi(x)$ holds and then try to find a $y$ such that $\phi'(x,y)$ holds, or show that the non-existence of such a $y$ would lead to a contradiction.
If you try to state them in words, both statements mean something like, "Any time we have an $x$ such that $\phi(x)$ holds, there is a $y$ such that $\phi'(x,y)$ holds."
Formally, the second alternative you give $$\forall x, \exists y \big( \phi(x)\implies \phi'(x,y)\big)$$ means the same thing, but it seems a little unnatural to me.  However, I'm by no means a logician.
A: Short answer : mathematical symbolism sometimes conceals conditional form in the same manner as natural language does ; in a proof, the proper conditional form of the goal has to be recovered in order to adopt the right  strategy ( consistng in assuming the antecedent , in order to derive the consequent, under the initial assumption). 



*

*The question is a grammatical one, and amounts to asking how to formalize sentences such as : 


[ Every X + relative clause] + Verb + Attribute / Object. 
[ An X + adjective} + Verb + Attribute/ Object. 
[ An X + participle clause] + Verb + Object/ Attribute
All these grammatical forms are abbreviating devices used by natural language; logic teaches us that the  logical structure ( beyond the surface grammar form) involves a conditional. 


*

*The point is that, mathematics also uses this abbreviating device. Sometimes, a change in typography ( with the use of indices) accompanies this sort of writing. 


For example, in order to say ( note the relative clauses below) : 
For all $\epsilon$ that is strictly greater than 0, there is a $\delta$ that is strictly greater than 0, such that if ($0 < | x-a| < \delta$) then ($ | f(x)-L| < \epsilon$)
one will write 
$\forall\epsilon_{(>0)}\exists \delta_{(>0)} [(0 < | x-a| < \delta)\rightarrow ( | f(x)-L| < \epsilon)]$. 
But this is an abbreviation, and in fact, it " hides" a conditional form: for all $\epsilon$ , if $\epsilon$ is strictly greater than 0, then, there exists some $\delta$ such that, if.... then... . 


*

*So how to formalize? 


[ Every X + relative clause] + Verb + Attribute / Object. 
Every natural number that is different from 0 is the successor of some natural number. 
$\forall (x) {[ (x\in\mathbb N) \wedge (x\neq0)] \rightarrow [\exists (y) (y\in\mathbb N) \wedge (x=S(y)]}$
or 
$\forall (x)_{ (x\in\mathbb N)} [ (x\neq0) \rightarrow (\exists (y) (y\in\mathbb N) \wedge (x=S(y)) ] $
[ An X + adjective} + Verb + Attribute/ Object. 
Every even integer  has an even square. 
$\forall(x) [( x \in \mathbb Z \wedge x/2\in\mathbb Z) \rightarrow ( x^2 / 2 \in \mathbb Z)] $
[ An X + participle clause  ] + Verb + Object/ Attribute
All sets having no element are identical ( with |A| = cardinal of set A) : 
$\forall (S)(T) [ (|S|=0 \wedge |T| = 0 ) \rightarrow ( S=T)$]
Note : there are certainly some parenthesis mistakes I haven't corrected. 
