Metamath Proof Explorer

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 . (Contributed by NM, 10-Jan-1993)

Ref Expression
Assertion ax-5 φ x φ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 vx setvar x
2 0 1 wal wff x φ
3 0 2 wi wff φ x φ