Axiom ax-5

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).

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct . (Contributed by NM, 10-Jan-1993)

	Ref	Expression
Assertion	ax-5	$$⊢\phi \to \forall x\phi$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		vx	$$setvarx$$
2	0 1	wal	$$wff\forall x\phi$$
3	0 2	wi	$$wff\left(\phi \to \forall x\phi \right)$$