Axiom ax-17 1537

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

This axiom is referenced by:  a17d  1538  nfv  1539  exlimiv  1609  equid  1712  ax16  1824  dvelimfALT2  1828  exlimdv  1830  ax11a2  1832  albidv  1835  exbidv  1836  ax11v  1838  ax11ev  1839  ax16i  1869  ax16ALT  1870  equvin  1874  19.9v  1882  19.21v  1884  alrimiv  1885  alrimdv  1887  alimdv  1890  eximdv  1891  19.23v  1894  pm11.53  1907  19.27v  1911  19.28v  1912  19.41v  1914  19.42v  1918  cbvalv  1929  cbvexv  1930  cbvexdh  1938  nexdv  1952  sbhb  1956  hbsbv  1957  sbco2vh  1961  nfsb  1962  equsb3lem  1966  equsb3  1967  sbn  1968  sbim  1969  sbor  1970  sban  1971  sbco3  1990  nfsbt  1992  sb9  1995  sbcom2v2  2002  sbcom2  2003  dfsb7  2007  sbid2v  2012  sbelx  2013  sbal  2016  sbal1  2018  sbex  2020  exsb  2024  dvelimALT  2026  dvelim  2033  dvelimor  2034  euf  2047  sb8euh  2065  euorv  2069  euex  2072  euanv  2099  mo4f  2102  moim  2106  moimv  2108  moanim  2116  mopick  2120  2eu4  2135  cleljust  2170  elsb1  2171  elsb2  2172  dveel1  2173  dveel2  2174  cleqh  2293  abeq2  2302  mpteq12  4112  bj-ex  15254  bj-inex  15399