Let $S$ be a set. Let $f$ be a function with $\operatorname{dom}(f)=S$. Let $P$ be a one-place property. Is the following statement well formed?
$$∀x \, x∈S → P(f(x))$$
How about another one?
$$\text{For any x∈S}, P(f(x)) \text{ holds}$$
Many theorems are of similar structure to these statements. But I see a problem here: logical implication is defined even when both arguments are false, but in this particular case if the first argument is false, the second argument is undefined.
Formally, are these 2 statements different or the same? I.e., does the latter statement, if we were to write it down formally, use logical implication or something else? How do mathematicians (I guess we're talking about logicians and maybe set theorists) solve this problem?
Update: The problem dissipates if I rewrite the statement more formally: $$\forall x \, x \in S \rightarrow \exists! y \exists q \, \left( q=(x, y) \land q \in f \land P(y) \right)$$