Description: Axiom of Distinctness. This axiom quantifies a variable over a formula
in which it does not occur. Axiom C5 in Megill p. 444 (p. 11 of the
preprint). Also appears as Axiom B6 (p. 75) of system S2 of Tarski
p. 77 and Axiom C5-1 of Monk2 p. 113.

(See comments in ax5ALT about the logical redundancy of ax-5 in the
presence of our obsolete axioms.)

This axiom essentially says that if x does not occur in ph ,
i.e. ph does not depend on x in any way, then we can add the
quantifier A. x to ph with no further assumptions. By sp , we
can also remove the quantifier (unconditionally).