Axiom ax-17 1526

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

This axiom is referenced by:  a17d  1527  nfv  1528  exlimiv  1598  equid  1701  ax16  1813  dvelimfALT2  1817  exlimdv  1819  ax11a2  1821  albidv  1824  exbidv  1825  ax11v  1827  ax11ev  1828  ax16i  1858  ax16ALT  1859  equvin  1863  19.9v  1871  19.21v  1873  alrimiv  1874  alrimdv  1876  alimdv  1879  eximdv  1880  19.23v  1883  pm11.53  1895  19.27v  1899  19.28v  1900  19.41v  1902  19.42v  1906  cbvalv  1917  cbvexv  1918  cbvexdh  1926  nexdv  1936  sbhb  1940  hbsbv  1941  sbco2vh  1945  nfsb  1946  equsb3lem  1950  equsb3  1951  sbn  1952  sbim  1953  sbor  1954  sban  1955  sbco3  1974  nfsbt  1976  sb9  1979  sbcom2v2  1986  sbcom2  1987  dfsb7  1991  sbid2v  1996  sbelx  1997  sbal  2000  sbal1  2002  sbex  2004  exsb  2008  dvelimALT  2010  dvelim  2017  dvelimor  2018  euf  2031  sb8euh  2049  euorv  2053  euex  2056  euanv  2083  mo4f  2086  moim  2090  moimv  2092  moanim  2100  mopick  2104  2eu4  2119  cleljust  2154  elsb1  2155  elsb2  2156  dveel1  2157  dveel2  2158  cleqh  2277  abeq2  2286  mpteq12  4087  bj-ex  14517  bj-inex  14662