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  1948  sbhb  1952  hbsbv  1953  sbco2vh  1957  nfsb  1958  equsb3lem  1962  equsb3  1963  sbn  1964  sbim  1965  sbor  1966  sban  1967  sbco3  1986  nfsbt  1988  sb9  1991  sbcom2v2  1998  sbcom2  1999  dfsb7  2003  sbid2v  2008  sbelx  2009  sbal  2012  sbal1  2014  sbex  2016  exsb  2020  dvelimALT  2022  dvelim  2029  dvelimor  2030  euf  2043  sb8euh  2061  euorv  2065  euex  2068  euanv  2095  mo4f  2098  moim  2102  moimv  2104  moanim  2112  mopick  2116  2eu4  2131  cleljust  2166  elsb1  2167  elsb2  2168  dveel1  2169  dveel2  2170  cleqh  2289  abeq2  2298  mpteq12  4101  bj-ex  14951  bj-inex  15096