Axiom ax-17 1579

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

This axiom is referenced by:  a17d  1580  nfv  1581  exlimiv  1651  equid  1753  equsexvw  1781  ax16  1866  dvelimfALT2  1870  exlimdv  1872  ax11a2  1874  albidv  1877  exbidv  1878  ax11v  1880  ax11ev  1881  ax16i  1911  ax16ALT  1912  equvin  1916  19.9v  1924  19.21v  1926  alrimiv  1927  alrimdv  1929  alimdv  1932  eximdv  1933  19.23v  1936  sbv  1949  pm11.53  1951  19.27v  1955  19.28v  1956  19.41v  1958  19.42v  1962  cbvalv  1973  cbvexv  1974  cbvexdh  1982  nexdv  1996  sbhb  2000  hbsbv  2001  sbco2vh  2005  nfsb  2006  equsb3lem  2010  equsb3  2011  sbn  2012  sbim  2013  sbor  2014  sban  2015  sbco3  2034  nfsbt  2036  sb9  2039  sbcom2v2  2046  sbcom2  2047  dfsb7  2051  sbid2v  2056  sbelx  2057  sbal  2060  sbal1  2062  sbex  2064  exsb  2068  dvelimALT  2070  dvelim  2077  dvelimor  2078  euf  2091  sb8euh  2109  euorv  2113  euex  2116  euanv  2144  mo4f  2147  moim  2151  moimv  2153  moanim  2161  mopick  2165  2eu4  2180  cleljust  2215  elsb1  2216  elsb2  2217  dveel1  2218  dveel2  2219  cleqh  2338  abeq2  2347  mpteq12  4212  bj-ex  16707  bj-inex  16850