what is a function? please. Axiom schema of replacement: Let the domain of the function $F$ be the set $A$. Then the range of $F$ (the values of $F(x)$ for all members $x$ of $A$) is also a set. &mdash; Tarski–Grothendieck set theory


I can't fully appreciated the axiom; for me, when talking about the function $F$, we should assume a domain and a range before.  So sounds that the axiom is circular.

So my question is: what is a function?
If a function is defined not through sets, then it sounds that “function” is more fundamental concept than “set.”
The usual statement of the axiom schema of replacement is as follows:

For any formula $\phi(x,y,p)$:
$$\forall p( \forall x,y,z(\phi(x,y,p)\land \phi(x,z,p) \to y = z) \to \forall X \exists Y \forall u(u \in Y \leftrightarrow \exists v(v \in X \land \phi(v,u,p))))$$

Here, $p$ is to be thought of as a &quot;parameter&quot;, e.g. used if $\phi(x,y,p)$ is the formula $y = (x,p)$; the resulting set $Y$ will depend on $p$. The first part expresses that $\phi(\cdot,\cdot,p)$ is a functional relation: any $x$ admits at most one $y$ such that $\phi(x,y,p)$.
It is this $\phi(x,y,p)$ that is referred to, sloppily, as a &quot;function&quot;. But we see that $\phi$ has to be of a rather more explicit form: it needs to be a formula that is expressible using the language of set theory, and we need to be able to verify that it constitutes a functional relation. Only then may we invoke replacement to conclude that $Y_p = \{y\mid\exists x: \phi(x,y,p)\}$ is a set.
We have thus crafted sort of a &quot;formal analogue&quot; of a &quot;function&quot;, by using certain formulae (which are syntactical objects) in place of certain sets (which are semantical objects). By imposing functionality, we ensure that our formal analogue behaves more or less like a function. However, we did not specify either &quot;domain&quot; or &quot;codomain&quot;, and they may very well not be sets (they can be empty, or consist of all sets!).
The unspecified domain and codomain are what separates a &quot;formal function&quot; from an &quot;internal function&quot;, using the standard &quot;suitable collection of ordered pairs&quot; definition.
Now why aren't &quot;formal functions&quot; more general than sets? This is because they are still expressed in terms of &quot;sets&quot; (rather, in terms of the variables $x,y,z,p,u,v,X,Y$, which we want to think of as sets). We cannot dispose of these variables and still sensibly talk about the formulae that we have called &quot;formal functions&quot; cq. &quot;functional relations&quot;.

What we have seen above is actually an example of a phenomenon that can be very confusing. We have seen &quot;functions&quot; that are of a different form than what our usual definition of function is. They can be &quot;too large&quot; to fit the usual definition of function.
We, external to the model of set theory, can reason about these &quot;functions&quot;. However, the model itself does not have the means to contemplate them as a single object. We say the &quot;function&quot; is external to the model. The usual definition of a function could appropriately (but at the expense of considerable tedium) be called an internal function, because the model is able to reason about it as a single object.
This internal vs. external doctrine comes back at many, sometimes unexpected places in logic, and can give rise to intuitively bewildering statements. You can think of the distinction between $A \vdash B$ and $A \to B$ in propositional calculus as a further example: the former is the external way of saying &quot;if $A$ holds, so does $B$&quot;, while the latter is its internal analogue. In propositional calculus, the two notions agree, but in more complicated systems, sometimes one can fail while the other holds (!).
A function $f: A \rightarrow B$ is just a subset $f \subseteq A \times B$ such that for every $a \in A$ there is a unique $b =: f(a) \in B$ with $(a,b) \in f$. Note that $A\times B$ exists as $A \times B = \{ (a,b) \mid a \in A, b \in B \}= \{ \ \{\ \{a\} \ ,\ \{a,b\}\ \} \mid a\in A, b \in B \} \subseteq \mathcal P(\mathcal P(A \cup B)) $, where $\mathcal P(X)$ denotes the power set of $X$.
Also note that we didn't make use of the axiom schema of replacement here.