Working in ZFC.
I've defined a function-like binary predicate $R$ on a proper class. It has to be recursive; i.e. $R(a,b)$ must usually depend on one or more $R(c,d)$ for some $c$s and $d$s calculated from $a$ and $b$. There is, however, no well-founded recursive, unary function that agrees with $R$ (i.e. there is no $F$ such that $y = F(x)$ iff $R(x,y)$).
So I've defined it like ZFC defines $\in$: I've added a new binary predicate symbol $R$ and defined axioms for it. Every axiom conforms to the schema $\forall x_1 . \dots \forall x_n . P_1(x_1) \wedge \dots \wedge P_n(x_n) \rightarrow Q(x_1,\dots,x_n) \rightarrow R(x_1,x_2)$. I think the salient facts are 1) that no axiom concludes that a set exists, only that $R$ relates two sets; and 2) $Q(x_1,\dots,x_n)$ is a formula that usually refers to $R$.
I'd like to prove that ZFC+R proves that no more sets exist than ZFC does. How can I do this?
(Also, is "conservative extension" the right term for this?)