Disjointed variables

Predicate calculus imposes some restrictions on the substitutions, which may be applied to some certain inference rules. In Russell this is reflected with the notion of disjointed variables:

axiom ax-17 (ph : wff, x : set) disjointed(x ph) {
    prop 1 : wff = |- ( ph → ∀ x ph ) ;;
}

Here variables x and ph are marked as disjointed. It means, that any usage of this axiom, when some substitution such that x and ph are substituted with expressions, which have common variables, is prohibited.