A common definition of function between two sets (or between two classes, when working in GBN) is based on the notion of "ordered pair". An ordered pair is some set-theoretic construction, denoted "$(a,b)$" where $a$ and $b$ are sets, with the property that
$(a,b)=(c,d)$ if and only if $a=c$ and $b=d$. There are many ways of achieving this; the most common is the Kuratowski definition of ordered pair:
Definition. If $a$ and $b$ are sets, then the ordered pair $(a,b)$ is the set
$$(a,b) = \Bigl\{ \{a\}, \{a,b\}\Bigr\}.$$
Note that $(a,b)$ is a set if $a$ and $b$ are sets. The Axiom of Pairing guarantees the existence of a set $P$ that contains $a$ and $b$ as elements; and then both $\{a\}$ and $\{a,b\}$ are elements of the power set of $P$, so $(a,b)$ is an element of the power set of the power set of $P$. Also:
Theorem. $(a,b) = (c,d)$ if and only if $a=c$ and $b=d$.
Proof. If $a=c$ and $b=d$, then $(a,b)=(c,d)$. Assume now that $(a,b)=(c,d)$. Then
$$\{a\} = \cap(a,b) = \cap(c,d) = \{c\},$$
so $a=c$. If $b=a$, then $(c,d) = (a,b) = \{\{a\}\}$, so $\{c,d\}=\{a\}$, hence $d=a=b=c$. Likewise, if $d=c$, then $a=b=c=d$.
If $a\neq b$ and $c\neq d$, then $\{b\} = \cup(a,b) - \cap(a,b) = \cup(c,d)-\cap(c,d) = \{d\}$, so $b=d$. QED
Now let $A$ and $B$ be sets (classes if you are in GBN). The cartesian product $A\times B$ of $A$ and $B$ is defined to be
$$A\times B = \{ (a,b) \mid a\in A, b\in B\}.$$
If $A$ and $B$ are sets, then so is $A\times B$: it is an element of $\mathcal{P}(\mathcal{P}(\mathcal{P}(A\cup B)))$.
Now we are ready:
Definition. Let $A$ and $B$ be sets (or classes). A function $f\colon A\to B$ is a subset (or subclass) $f\subseteq A\times B$ such that:
- For all $a\in A$ there exists $b\in B$ such that $(a,b)\in f$; and
- For all $a\in A$ and $b,b'\in B$, if $(a,b)\in f$ and $(a,b')\in f$, then $b=b'$.
The idea is that $f$ "assigns" $a\in A$ to $b\in B$ if and only if $(a,b)\in f$. In that case, we write $f(a)=b$ (to mean $(a,b)\in f$).
The problem with your last bullet point is really the first bullet point. You seem to be confusing "function" with "function you can name".
The problem with the Axiom of Choice is more subtle than the notion of "being able to write down something". For example, if you restrict your universe to the "constructible sets" (see Wikipedia's article) of ZF (without assuming AC), then the Axiom of Choice is true for the constructible sets.
The connection between your example and the more general definition is that $\bigcup\{a,b\}=a\cup b$. Written out in all its gory details, this is
$$\bigcup\Big\{\{1,2,3\},\{4,5\}\Big\}=\{1,2,3\}\cup\{4,5\}=\{1,2,3,4,5\}\;.$$
Let’s check that against the definition:
$$\begin{align*}
&\bigcup\Big\{\{1,2,3\},\{4,5\}\Big\}\\
&\qquad=\left\{x:\text{there exists an element }y\in\Big\{\{1,2,3\},\{4,5\}\Big\}\text{ such that }x\in y\right\}\\
&\qquad=\Big\{x:x\in\{1,2,3\}\text{ or }x\in\{4,5\}\Big\}\\
&\qquad=\{1,2,3\}\cup\{4,5\}\\
&\qquad=\{1,2,3,4,5\}\;.
\end{align*}$$
Take a slightly bigger example. Let $a,b$, and $c$ be any sets; then
$$\begin{align*}
\bigcup\{a,b,c\}&=\Big\{x:\text{there exists an element }y\in\{a,b,c\}\text{ such that }x\in y\Big\}\\
&=\{x:x\in a\text{ or }x\in b\text{ or }x\in c\}\\
&=a\cup b\cup c\;.
\end{align*}$$
One more, even bigger: for $n\in\Bbb N$ let $A_n$ be a set, and let $\mathscr{A}=\{A_n:n\in\Bbb N\}$. Then
$$\begin{align*}
\bigcup\mathscr{A}&=\Big\{x:\text{there exists an }n\in\Bbb N\text{ such that }x\in A_n\Big\}\\
&=\{x:x\in A_0\text{ or }x\in A_1\text{ or }x\in A_2\text{ or }\dots\}\\
&=A_0\cup A_1\cup A_2\cup\dots\\
&=\bigcup_{n\in\Bbb N}A_n\;.
\end{align*}$$
Best Answer
Coin flips don't work because you need to decide which sock goes for "heads" and which one for "tails". Once you've made that assignment you don't need the coin anymore; just assume you always get heads.