Axiom ax-17 1460

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	⊢ (𝜑 → ∀𝑥𝜑)

Distinct variable group:   𝜑,𝑥

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wal 1283	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  a17d  1461  nfv  1462  exlimiv  1530  equid  1630  ax16  1736  dvelimfALT2  1740  exlimdv  1742  ax11a2  1744  albidv  1747  exbidv  1748  ax11v  1750  ax11ev  1751  ax16i  1781  ax16ALT  1782  equvin  1786  19.9v  1794  19.21v  1796  alrimiv  1797  alrimdv  1799  alimdv  1802  eximdv  1803  19.23v  1806  pm11.53  1818  19.27v  1822  19.28v  1823  19.41v  1825  19.42v  1829  cbvalv  1837  cbvexv  1838  cbvexdh  1844  nexdv  1854  cleljust  1856  sbhb  1859  hbsbv  1860  sbco2v  1864  nfsb  1865  equsb3lem  1867  equsb3  1868  sbn  1869  sbim  1870  sbor  1871  sban  1872  sbco3  1891  nfsbt  1893  elsb3  1895  elsb4  1896  sb9  1898  sbcom2v2  1905  sbcom2  1906  dfsb7  1910  sbid2v  1915  sbelx  1916  sbal  1919  sbal1  1921  sbex  1923  exsb  1927  dvelimALT  1929  dvelim  1936  dvelimor  1937  dveel1  1939  dveel2  1940  euf  1948  sb8euh  1966  euorv  1970  euex  1973  euanv  2000  mo4f  2003  moim  2007  moimv  2009  moanim  2017  mopick  2021  2eu4  2036  cleqh  2182  abeq2  2191  mpteq12  3887  bj-ex  11005  bj-inex  11140