How do "informal" statements in set theory correspond to formal statements in (e.g.) the language of ZFC?

Question

I posted a question on here a few days ago about the formal definition of "well-definedness", but I don't think that question really got at the heart of what I was confused about. Here is an attempt to ask something more specific and concrete.

Suppose I have a function $f: A \to B$, an element $a\in A$, and a subset $U\subseteq B$. Informally, I can make a claim like "$f(a)\in U$". But, theoretically, this can all be formalized in (e.g.) ZFC within first-order logic. But I am not sure how exactly this should be done. It seems that there are multiple formal statements that this informal statement could correspond to, and I'm not sure which one is right. The problem stems from the fact that $f$ is a function within the theory of ZFC (it's a set of ordered pairs satisfying various properties), it is not a function symbol in the language of ZFC, and so we cannot directly name "$f(a)$" in our formula. Actually, we can't name "$a$" either. So a work-around is required, and this is where I get confused.

Let $\phi_a(x)$ be a formula in one free variable which uniquely picks out $a$, let $\phi_f(x)$ be a formula which uniquely picks out $f$ (the set of ordered pairs), and $\psi_U(x)$ be a formula that picks out elements of $U$. Then one way we could formalize "$f(a)\in U$" seems to be $$\forall x (\phi_a(x) \to \exists y\exists z( \phi_f(y) \land (x, z)\in y \land \psi_U(z)) ). $$ But I'm not sure if this is right, because it also seems that $$\forall x (\phi_a(x) \to \exists y\forall z( (\phi_f(y) \land (x, z)\in y ) \to \psi_U(z)) ). $$ would work. These are both equivalent (I think), because $f$ is a function and so in fact $f(a)$ is unique. Various other combinations of quantifiers work as well. Maybe it doesn't matter which one we pick, since they're equivalent? Then again, maybe we need to specify the uniqueness of $f(a)$ within the formula itself, as this uniqueness might be used later in a proof. Thus $$\forall x (\phi_a(x) \to \exists y(\exists z( \phi_f(y) \land (x, z)\in y \land \psi_U(z)) \land \forall w( (\phi_f(y) \land (x, w)\in y ) \to \psi_U(w))) )$$ or something to that effect. Or perhaps the quantifier in front of $y$ should be "$\forall$".

Anyway, the point is that I am not sure how to take an informal statement involving objects named and defined within the theory of ZFC and translate it into a formula in the language of ZFC. Can someone help me with this?

Answer 1

A function is a subset of the cartesian product; thus, the first step is to state that $f \subseteq A \times B$.

But this holds for every relation; thus, we have to add the "functionality" condition: $∀x,y,z[(x,y)∈f \land (x,z)∈f \to y=z]$.

Thus, the result will be:

$$∀A,B,U,a,b \ [ (f \subseteq A \times B) \land ∀x,y,z[(x,y)∈f \land (x,z)∈f \to y=z] ∧ a∈A \land U \subseteq B \land (a,b)∈f \to b∈U]$$

Note: in order to use the $f(x)$ notation for a function $f$, we have to add to the theory the definitional axiom: $f(x)=y \leftrightarrow [\exists ! z \ ( (x, z) \in f) \land (x, y) \in f ]$.