Axiom ax-17 1519

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

This axiom is referenced by:  a17d  1520  nfv  1521  exlimiv  1591  equid  1694  ax16  1806  dvelimfALT2  1810  exlimdv  1812  ax11a2  1814  albidv  1817  exbidv  1818  ax11v  1820  ax11ev  1821  ax16i  1851  ax16ALT  1852  equvin  1856  19.9v  1864  19.21v  1866  alrimiv  1867  alrimdv  1869  alimdv  1872  eximdv  1873  19.23v  1876  pm11.53  1888  19.27v  1892  19.28v  1893  19.41v  1895  19.42v  1899  cbvalv  1910  cbvexv  1911  cbvexdh  1919  nexdv  1929  sbhb  1933  hbsbv  1934  sbco2vh  1938  nfsb  1939  equsb3lem  1943  equsb3  1944  sbn  1945  sbim  1946  sbor  1947  sban  1948  sbco3  1967  nfsbt  1969  sb9  1972  sbcom2v2  1979  sbcom2  1980  dfsb7  1984  sbid2v  1989  sbelx  1990  sbal  1993  sbal1  1995  sbex  1997  exsb  2001  dvelimALT  2003  dvelim  2010  dvelimor  2011  euf  2024  sb8euh  2042  euorv  2046  euex  2049  euanv  2076  mo4f  2079  moim  2083  moimv  2085  moanim  2093  mopick  2097  2eu4  2112  cleljust  2147  elsb1  2148  elsb2  2149  dveel1  2150  dveel2  2151  cleqh  2270  abeq2  2279  mpteq12  4072  bj-ex  13797  bj-inex  13942