In the following paper, there is a theory called $^*ZFC$ in the language $(^*,\in)$. The *-map is (more or less) defined on the Von Neuman hierarchy $S$ and verifies the following axiom schemata true for all $\in$-formula $\phi$ : $$\forall a_1,...,a_n \in S, \phi^S(a_1,...,a_n) \Leftrightarrow \phi^I(^*a_1,...,^*a_n)$$ where $I$ is the class of internal elements (that is those included in a certain $^*b$ with $b\in S$), and $\phi^S$ (respectively $\phi^I$) is $\phi$ relativized to $S$ (respectively $I$).
There is a process usual in mathematics that I now describe, which is usually done for $ZFC$ but that we do here for $^*ZFC$. One can add functions symbols to make $^*ZFC$ richer, for example, if $^*ZFC \vdash \forall x \forall y \exists ! z,F(x,y,z) $, one can create the $(^*ZFC)^+$, a L+-theory, where L+ is L to which we add a function symbol f with arity 2, and where $(^*ZFC)^+$ is $^*ZFC$ to which we add the formulas $\forall x \forall y F(x,y,f(x,y)) $. It is easy to prove that for all F L-formula which are closed, we have $$^*ZFC\vdash F$$ if and only if we have $$(^*ZFC)^+ \vdash F$$ And for all L+-formula F, there is a L-formula F' such that $(^*ZFC)^+ \vdash F$ if and only if $(^*ZFC)^+ \vdash F'$, so we can work in everyday mathematics as if it were in $^*ZFC$, although we use symbols such as $\cos$, $\sin(a)$, $\emptyset$, $\left\{a,b\right\}$ and so on.
Now, what I wonder is the behaviour of formulas in the new language (not just $\in$-formulas), when we use the transfert principle stated above. Is it true for all the new formulas ? Just some ? Does the formula $F$ which defines the new symbol has to verify certain conditions ?