Axiom ax-17 1575

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

This axiom is referenced by:  a17d  1576  nfv  1577  exlimiv  1647  equid  1749  equsexvw  1777  ax16  1862  dvelimfALT2  1866  exlimdv  1868  ax11a2  1870  albidv  1873  exbidv  1874  ax11v  1876  ax11ev  1877  ax16i  1907  ax16ALT  1908  equvin  1912  19.9v  1920  19.21v  1922  alrimiv  1923  alrimdv  1925  alimdv  1928  eximdv  1929  19.23v  1932  sbv  1945  pm11.53  1947  19.27v  1951  19.28v  1952  19.41v  1954  19.42v  1958  cbvalv  1969  cbvexv  1970  cbvexdh  1978  nexdv  1992  sbhb  1996  hbsbv  1997  sbco2vh  2001  nfsb  2002  equsb3lem  2006  equsb3  2007  sbn  2008  sbim  2009  sbor  2010  sban  2011  sbco3  2030  nfsbt  2032  sb9  2035  sbcom2v2  2042  sbcom2  2043  dfsb7  2047  sbid2v  2052  sbelx  2053  sbal  2056  sbal1  2058  sbex  2060  exsb  2064  dvelimALT  2066  dvelim  2073  dvelimor  2074  euf  2087  sb8euh  2105  euorv  2109  euex  2112  euanv  2140  mo4f  2143  moim  2147  moimv  2149  moanim  2157  mopick  2161  2eu4  2176  cleljust  2211  elsb1  2212  elsb2  2213  dveel1  2214  dveel2  2215  cleqh  2334  abeq2  2343  mpteq12  4195  bj-ex  16551  bj-inex  16694