Axiom ax-17 1416

Description: Axiom to quantify 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.

(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 1240	. 2 wff ∀xφ
4	1, 3	wi 4	1 wff (φ → ∀xφ)

This axiom is referenced by:  a17d  1417  nfv  1418  exlimiv  1486  equid  1586  ax16  1691  dvelimfALT2  1695  exlimdv  1697  ax11a2  1699  albidv  1702  exbidv  1703  ax11v  1705  ax11ev  1706  ax16i  1735  ax16ALT  1736  equvin  1740  19.9v  1748  19.21v  1750  alrimiv  1751  alrimdv  1753  alimdv  1756  eximdv  1757  19.23v  1760  pm11.53  1772  19.27v  1776  19.28v  1777  19.41v  1779  19.42v  1783  cbvalv  1791  cbvexv  1792  cbvexdh  1798  nexdv  1808  cleljust  1810  sbhb  1813  hbsbv  1814  sbco2v  1818  nfsb  1819  equsb3lem  1821  equsb3  1822  sbn  1823  sbim  1824  sbor  1825  sban  1826  sbco3  1845  nfsbt  1847  elsb3  1849  elsb4  1850  sb9  1852  sbcom2v2  1859  sbcom2  1860  dfsb7  1864  sbid2v  1869  sbelx  1870  sbal  1873  sbal1  1875  sbex  1877  exsb  1881  dvelimALT  1883  dvelim  1890  dvelimor  1891  dveel1  1893  dveel2  1894  euf  1902  sb8euh  1920  euorv  1924  euex  1927  euanv  1954  mo4f  1957  moim  1961  moimv  1963  moanim  1971  mopick  1975  2eu4  1990  cleqh  2134  abeq2  2143  mpteq12  3831  bj-ex  9237  bj-inex  9362