Can we allow defined predicates and functions in reflection? By Reflection I mean the following schema:
Reflection: $$\forall X \, (\varphi \implies \exists  \alpha : \varphi^{V_\alpha})$$
where $\varphi$ is a first order formula (defined predicates and functions allowed) in which only symbol "$X$" occurs free, $\varphi^{V_\alpha}$ is the "$\in {V_\alpha}$" bounded form of $\varphi$.
$V_\alpha$ is defined in the customary manner as the set of all subsets of elements of the range of a function from an ordinal $\alpha$ where the image of a successor is the power set of the image of its predecessor, and the image of a limit is the union of all images of prior ordinals. And ordinal is defined after von Neumann as a transitive set well ordered by $\in$.
The point here is that we are allowing the use of defined predicate and function symbols, as long as the formula remain first order, i.e. no quantification allowed over them.
Is reflection here a theorem scheme of $\sf ZF$?
 A: The first answer took care of the case where "Reflection" was a scheme of formulas in the language of ZF. Now we consider what we now think was the intent of the questioner.
We expand the language of ZF by introducing a predicate symbol P and a function symbol F
for each formula  in the language of ZF. We also add additional axioms:
∀x1,...,xn(P(x1,...,xn)<-->(x1,...,xn)) where x1,...,xn are the free variables of .
∀x1,...,xn,y(∀z(((x1,...,xn,z)<-->y=z)-->F(x1,....xn)=y))
where x1,...,xn,y are the free variables of 
∀x1,...,xn,y(((x1,...,xn,y)∧∃z(z≠y∧(x1,...,xn,z)))-->F(x1,...,xn)=0)
where x1,...,xn,y are the free variables of 
Call this theory ZZF.
"Reflection" holds in ZZF.
Proof:Let  be a formula in the language of ZZF whose only free variable is X. Let A be the set of formulas  such that P is a symbol of . Let B be the set of formulas  such that F is a symbol of . To each term t ocurring in  we shall associate a variable vt where if s and t are not variables then
vs=vt iff s=t, and vs is not a variable of .
To each term we will also associate a formula ft. We will do this inductively as follows:
if w is a variable then  vw=w and fw is w=w.
if s=F(t1,...,tn) then
fs is f(t1)∧...∧f(tn)∧(v(t1),...,v(tn),v(s))
For each subformula θ of  we define a formula  θ*  in the language of ZF as follows:
(t1=t2)* is f(t1)∧f(t2)∧v(t1)=v(t2)
(t1∈t2)* is f(t1)∧f(t2)∧v(t1)∈v(t2)
(P(t1,...,tn))* is f(t1)∧...∧f(tn)∧(v(t1),...,v(tn))
(θ1∧θ2)* is (θ1)∧(θ2)
(¬θ)* is ¬(θ*)
(∃xθ)* is ∃x(θ*)
We note that θ*<-->θ for all subformulas θ of .
Now suppose (X).
By the usual notion of reflection there is an ordinal  such that X∈V, V reflects *, and V reflects all formulas of A and B.
Then *(X) holds with quantifiers relativized to V.
Therefore (X) holds relativized to V, since relativized to V, (X)<-->*(X).
A: Each instance of the scheme referred to as  Reflection  is provable in ZF.
Suppose $\psi$ holds for some $X$. By the usual notion of reflection there is an ordinal $\alpha$ such that $X \in V_\alpha$  and $\forall y \, (y \in V_\alpha \implies ((V_\alpha \models \psi(y)) \iff \psi(y)))$. In particular $V_\alpha\models\psi(X)$.
Let $T$ be the theory axiomatized by extensionality, pairing, union, power set,
separation, and the scheme referred to as Reflection in this question.
Then $\operatorname{Con}(T)$ is provable in ZF.
Proof: For each set $s$, let
\begin{align*}
\mathsf A(s)=\{c \mid{} &c \text { is the least ordinal with } \\
& V_c\models \psi(x) \text { for some "formula" } \psi \land x \in s\}.
\end{align*}
Define a sequence $b$ of ordinals by $$b_0=0 \\ b_{n+1}=A(b_n).$$ Let $$\alpha =\bigcup \{b_n \mid n \in \omega\}.$$ Then the statement that "$T$ holds in $V_\alpha$" holds.
