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 36929 about the logical redundancy of ax-5 1913
in the
presence of our obsolete axioms.)
This axiom essentially says that if 𝑥 does not occur in 𝜑,
i.e. 𝜑 does not depend on 𝑥 in any
way, then we can add the
quantifier ∀𝑥 to 𝜑 with no further assumptions. By sp 2176, we
can also remove the quantifier (unconditionally).
For an explanation of disjoint variable conditions, see
https://us.metamath.org/mpeuni/mmset.html#distinct 2176. (Contributed by
NM, 10-Jan-1993.) |