Axiom ax-17 1616

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 ax17o 2157 about the logical redundancy of ax-17 1616 in the presence of our obsolete axioms.)

This axiom essentially says that if x does not occur in φ, i.e. φ does not depend on x in any way, then we can add the quantifier ∀x to φ with no further assumptions. By sp 1747, we can also remove the quantifier (unconditionally). (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ax-17	⊢ (φ → ∀xφ)

Distinct variable group:   φ,x

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff φ
2		vx	. . 3 setvar x
3	1, 2	wal 1540	. 2 wff ∀xφ
4	1, 3	wi 4	1 wff (φ → ∀xφ)

This axiom is referenced by:  a17d  1617  ax17e  1618  nfv  1619  alimdv  1621  eximdv  1622  albidv  1625  exbidv  1626  alrimiv  1631  alrimdv  1633  19.9v  1664  spimvw  1669  equidOLD  1677  spnfwOLD  1692  spw  1694  19.3vOLD  1696  alcomiw  1704  hbn1w  1706  ax11wlem  1720  sp  1747  spOLD  1748  dvelimhw  1849  ax12olem1  1927  ax12olem2  1928  ax12olem6  1932  ax10lem2  1937  dvelimv  1939  a16g  1945  ax11a2  1993  cleljust  2014  dvelim  2016  ax16ALT  2047  ax11vALT  2097  dvelimALT  2133  ax17o  2157  dveeq2-o  2184  dveeq1-o  2187  ax11el  2194  ax11a2-o  2202  eujustALT  2207  cleqh  2450  abeq2  2459  hboprab  5563  mpteq12  5658