Axiom ax-17 1550

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

This axiom is referenced by:  a17d  1551  nfv  1552  exlimiv  1622  equid  1725  ax16  1837  dvelimfALT2  1841  exlimdv  1843  ax11a2  1845  albidv  1848  exbidv  1849  ax11v  1851  ax11ev  1852  ax16i  1882  ax16ALT  1883  equvin  1887  19.9v  1895  19.21v  1897  alrimiv  1898  alrimdv  1900  alimdv  1903  eximdv  1904  19.23v  1907  pm11.53  1920  19.27v  1924  19.28v  1925  19.41v  1927  19.42v  1931  cbvalv  1942  cbvexv  1943  cbvexdh  1951  nexdv  1965  sbhb  1969  hbsbv  1970  sbco2vh  1974  nfsb  1975  equsb3lem  1979  equsb3  1980  sbn  1981  sbim  1982  sbor  1983  sban  1984  sbco3  2003  nfsbt  2005  sb9  2008  sbcom2v2  2015  sbcom2  2016  dfsb7  2020  sbid2v  2025  sbelx  2026  sbal  2029  sbal1  2031  sbex  2033  exsb  2037  dvelimALT  2039  dvelim  2046  dvelimor  2047  euf  2060  sb8euh  2078  euorv  2082  euex  2085  euanv  2112  mo4f  2115  moim  2119  moimv  2121  moanim  2129  mopick  2133  2eu4  2148  cleljust  2183  elsb1  2184  elsb2  2185  dveel1  2186  dveel2  2187  cleqh  2306  abeq2  2315  mpteq12  4135  bj-ex  15837  bj-inex  15981