In a Hilbert-style axiomatization of first-order logic (FOL), there is a rule for variable substitution but I don't see any rule for substituting predicate symbols. Consider a theorem like:
$\forall x(P(x)) \lor \forall x(Q(x)) \rightarrow \forall x(P(x) \lor Q(x))$
Intuitively I would think that I should be able to substitute $\lnot P(x)$ for $P(x)$ in the above and still get a valid formula (since the theorem was valid under all interpretations to begin with). Even more, I may want to substitute, say, $P(x)\land Q(x)$ for $P(x)$ and $P(x)\leftrightarrow Q(x)$ for $Q(x)$ if it were allowed.
In propositional calculus (PC) there is the rule of uniform substitution for propositional symbols, which could be considered predicates of arity 0. But in FOL this rule seems to be "burried" by defining all PC tautologies as an axiom schema, and then apparently I can no longer apply the rule.
So is it possible to define such an admissible (derivable?) rule for uniform substitution of predicate symbols in FOL? If yes, what would be the rule in the most general case and how would one prove it? If no, can you give an example where the application of such a rule to a provable formula would result in an invalid formula, or perhaps why it does not make sense to have such a rule?