I want to prove these two definitions of AoC are equivalent in ZF. As Set Theory is kinda confusing me at the moment, I'd like someone to verify my proofs.
Definition 1. For any relation $R$ there is a function $F \subseteq R$ with $\textrm{dom} \ F = \textrm{dom} \ R$.
Definition 2. For any set $I$ and any function $F$ with domain $I$, if $(\forall i \in I)(F(i) \ne \varnothing)$, $\prod\limits_{i \in I} F(i) \ne \varnothing$ (where $\prod$ is the generalized Cartesian product).
Assume Definition 2. Let $R$ be a relation and, for any $r \in \textrm{dom} \ R$, let $R_r := \{(x, y) \in R : x = r\}$. Let $F := \{(r, R_r); \ r \in \textrm{dom} \ R\}$. I think it's easy to show all of these are sets. Also, $F$ is a function by definition and clearly $F(r) \ne \varnothing; \ \forall r \in \textrm{dom} \ R$. Then the function guaranteed to exist by Definition 2 satisfies Definition 1.
Assume Definition 1. Let $F$ be some function defined on $I$. Define a relation $R$ so that, for every $i$ in $I$, $R$ contains all of the elements of $\{i\} \times F(i)$ (and nothing else). This is a set because it's a definable subset of $I \times \bigcup \bigcup F$. Then the function guaranteed to exist by Definition 1 satisfies Definition 2.
Although, why is $R$ a definable subset of $I \times \bigcup \bigcup F$? I've noticed that I don't actually know how to show that, given a relation $R$, the range of $R$ is a definable subset of $\bigcup \bigcup R$. I'm using Enderton's book and he doesn't prove this, merely states the set exists because it's a subset of $\bigcup \bigcup R$. Do we allow parameters in our formulas here? As in, can I reference any set as if it were a constant of the underlying language? Because I don't think it's possible to do this without them.