Axiom ax-17 1506

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 1329	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  a17d  1507  nfv  1508  exlimiv  1577  equid  1677  ax16  1785  dvelimfALT2  1789  exlimdv  1791  ax11a2  1793  albidv  1796  exbidv  1797  ax11v  1799  ax11ev  1800  ax16i  1830  ax16ALT  1831  equvin  1835  19.9v  1843  19.21v  1845  alrimiv  1846  alrimdv  1848  alimdv  1851  eximdv  1852  19.23v  1855  pm11.53  1867  19.27v  1871  19.28v  1872  19.41v  1874  19.42v  1878  cbvalv  1889  cbvexv  1890  cbvexdh  1898  nexdv  1908  cleljust  1910  sbhb  1913  hbsbv  1914  sbco2vh  1918  nfsb  1919  equsb3lem  1923  equsb3  1924  sbn  1925  sbim  1926  sbor  1927  sban  1928  sbco3  1947  nfsbt  1949  elsb3  1951  elsb4  1952  sb9  1954  sbcom2v2  1961  sbcom2  1962  dfsb7  1966  sbid2v  1971  sbelx  1972  sbal  1975  sbal1  1977  sbex  1979  exsb  1983  dvelimALT  1985  dvelim  1992  dvelimor  1993  dveel1  1995  dveel2  1996  euf  2004  sb8euh  2022  euorv  2026  euex  2029  euanv  2056  mo4f  2059  moim  2063  moimv  2065  moanim  2073  mopick  2077  2eu4  2092  cleqh  2239  abeq2  2248  mpteq12  4011  bj-ex  12969  bj-inex  13105