In the definition of Strong Feferman Set Theory, what does this phrase mean? In this post, Mike Shulman talks about Strong Feferman Set Theory, arguing that it deals with the foundational issues raised by category theory in an especially straightforward manner.
Mike explains:

To ZFC (or your favorite set theory) we add a constant symbol $U$
  together with the axiom “$U$ is a universe,” and also an axiom schema
  stating that for any statement $\varphi$, all of whose parameters are
  in $U$ but which does not mention $U$ explicitly, we have $\varphi^U \Leftrightarrow \varphi$.

What does the expression 'all of whose parameters are in $U$ but which does not mention $U$ explicitly' actually mean?
 A: Here is an example of "parameters". Suppose we are trying to write an axiom that for all sets $x,y$ there is a $z = \{x,y\}$. We would write the axiom as:
$$
(\forall x)(\forall y)(\exists z)(\forall w)[w \in z \leftrightarrow w = x \lor w = y]
$$
Here $x$ and $y$ are called (informally) the "parameters" of this axiom, because they are the sets upon which the constructed set $z$ will depend.
The axiom scheme in the question is trying to say that the elements of $U$ have the same properties from the perspective of $U$ that the do from the perspective of the entire universe. For example, a set $x$ is "countable in $U$" if and only if it is countable:
$$
(\forall x \in U) \left [ (\exists f \in U)(\text{$f$ is a bijection from $x$ to $\omega$}) \leftrightarrow (\exists g)(\text{$g$ is a bijection from $x$ to $\omega$})\right ]
$$
This can be put into the form $(\forall x \in U)[\phi^U(x) \leftrightarrow \phi(x)]$, so $x$ is a "parameter" of that formula $\phi$ in this scheme. 
A: It means that the symbol $U$ does not appear in $\varphi$, and the schema is something like that:
$$\forall p_1\in U\ldots\forall p_n\in U(\varphi^U(p_1,\ldots,p_n)\leftrightarrow\varphi(p_1,\ldots,p_n))$$
Where $\varphi^U$ is the relativized formula (which is a recursive syntactical modification of the formula $\varphi$ which happens at the meta-theory).
A: A parameter is basically some value that is a part of the formula. For example, take the statement "every subset of $\mathbb R$ with an upper bound has a least upper bound in $\mathbb R$". Roughly speaking, this can be realized as a formula "every subset of $x$ with an upper bound has a least upper bound $x$" with parameter $x := \mathbb R$.
Now, in this example, we do not need to use a parameter if we do not want to, since we can just include the definition of $\mathbb R$ in the statement itself. This is not always the case, however. For example, if a parameter is not definable in the language you are using, it obviously can not just be replaced with its definition.
So, what the axiom is saying is that the formula $\phi$ does not just need to be a sequence of set theoretic symbols, but can include any set as well.
This also has an important consequence for what you can and can not proof. For any formula $\phi$, we have a single axiom asserting that $\phi^U \iff \phi$ for all possible parameters, instead of an axiom of each combination of parameters. Since proofs can only invoke a finite number of axioms, this makes a difference.
