Axiom ax-17 1471

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

This axiom is referenced by:  a17d  1472  nfv  1473  exlimiv  1541  equid  1641  ax16  1748  dvelimfALT2  1752  exlimdv  1754  ax11a2  1756  albidv  1759  exbidv  1760  ax11v  1762  ax11ev  1763  ax16i  1793  ax16ALT  1794  equvin  1798  19.9v  1806  19.21v  1808  alrimiv  1809  alrimdv  1811  alimdv  1814  eximdv  1815  19.23v  1818  pm11.53  1830  19.27v  1834  19.28v  1835  19.41v  1837  19.42v  1841  cbvalv  1849  cbvexv  1850  cbvexdh  1856  nexdv  1866  cleljust  1868  sbhb  1871  hbsbv  1872  sbco2v  1876  nfsb  1877  equsb3lem  1879  equsb3  1880  sbn  1881  sbim  1882  sbor  1883  sban  1884  sbco3  1903  nfsbt  1905  elsb3  1907  elsb4  1908  sb9  1910  sbcom2v2  1917  sbcom2  1918  dfsb7  1922  sbid2v  1927  sbelx  1928  sbal  1931  sbal1  1933  sbex  1935  exsb  1939  dvelimALT  1941  dvelim  1948  dvelimor  1949  dveel1  1951  dveel2  1952  euf  1960  sb8euh  1978  euorv  1982  euex  1985  euanv  2012  mo4f  2015  moim  2019  moimv  2021  moanim  2029  mopick  2033  2eu4  2048  cleqh  2194  abeq2  2203  mpteq12  3943  bj-ex  12375  bj-inex  12510