I have been self-studying logic and set theory and I'm a bit confused in how to write certain mathematical statements. I think I have grasped somewhat the difference between conditional/material implication, denoted frequently by "$\to$", and semantic consequence, denoted usually by "$\Longrightarrow$" or "$\models$".
My question is the following: in defining what it means for a function $f:A\to B$ to be injective, one could write
$f:A\to B$ is injective $\Longleftrightarrow (\forall x\in A) (\forall y\in A) (f(x) = f(y) \to x=y)$
Now suppose you have a function $g:A\to B$ such that $g$ is injective. Then one would write that for all $x\in A$ and for all $y\in A$,
$g(x) = g(y) \Longrightarrow x=y$.
But it doesn't seem like you could write
$(\forall x\in A)(\forall y\in A) (g(x) = g(y) \Longrightarrow x=y)$
since the above wouldn't be a wff, the symbol "$\Longrightarrow$" not being part of the object language.
To get to the point, how would one make logic statements involving quantifiers and logical relations such as "$\Longrightarrow$" or "$\Longleftrightarrow$" ? Do you simply not use quantifiers and just write things in plain english such as "for all $x\in A$..." ?