Defining Surjection as an Implication Is the following logical notation valid in describing the condition for a function $f$ being surjective? If $f: A \rightarrow B$ is a function, then $f$ is surjective if
$$\forall y, \exists x \in A \, : \, y \in B \implies y=f(x)$$
I think it is valid, because it seems equivalent to the traditional definition of surjection where the implication is implicit in the definition.
 A: If $A = B = \emptyset$, the empty function $f = \emptyset \subseteq A \times B$ is a surjection of $A$ onto $B$, but your formula:
$$\forall y \exists x \in A (y \in B \implies y=f(x))$$
which means
$$\forall y \exists x (x \in A \land (y \in B \implies y=f(x)))$$
is false in that case. You need to say:
$$\forall y (y \in B \implies (\exists x \in A (y=f(x))))$$
which is equivalent to the short-hand form:
$$\forall y \in B \exists x \in A (y=f(x))$$
(which is what I think you had in mind when you referred to the "traditional definition" with implicit implications).
A: Yes, it's valid. It's equivalent to the usual definition:
$$
\text{$f: A \rightarrow B$ is a surjection} \iff \forall y \in B, \exists x \in A : y = f(x)
$$
Anytime you have
"$\forall y, y \in S \implies \text{something about $y$}$"
it's the same as
"$\forall y \in S, \text{something about $y$}$"
I think that one may be defined in terms of the other, deep down in the bowels of whatever set theory you're using.
A: Yes, it is equivalent (edit if you assume that $A$ is not empty, as Rob Arthan pointed out) although someone could complain on the fact it would be more natural to write it as 
$$\forall y (y \in B \Rightarrow \exists x (x \in A \land f(x)=y))$$
The difference is psycological more than logical and stands in the fact that your form becomes in natural language: for each $y$ there is an $x \in A$ such that


*

*$y \in B$ and $y=f(x)$;

*or $y \not \in B$ (and $x$ can be any element of $A$, $f(x)=y$ won't be ever verified but that's not a problem because the left part in the implication is false).


The form I wrote above instead becomes (in natural language):
for all $y$ if $y \in B$ then there is an $x \in A$ such that $y=f(x)$.
P.s.: Now I'm wondering on whether these two formulas are equivalent in construtive mathematics.
