Axiom ax-17 1507

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

This axiom is referenced by:  a17d  1508  nfv  1509  exlimiv  1578  equid  1678  ax16  1786  dvelimfALT2  1790  exlimdv  1792  ax11a2  1794  albidv  1797  exbidv  1798  ax11v  1800  ax11ev  1801  ax16i  1831  ax16ALT  1832  equvin  1836  19.9v  1844  19.21v  1846  alrimiv  1847  alrimdv  1849  alimdv  1852  eximdv  1853  19.23v  1856  pm11.53  1868  19.27v  1872  19.28v  1873  19.41v  1875  19.42v  1879  cbvalv  1890  cbvexv  1891  cbvexdh  1899  nexdv  1909  cleljust  1911  sbhb  1914  hbsbv  1915  sbco2vh  1919  nfsb  1920  equsb3lem  1924  equsb3  1925  sbn  1926  sbim  1927  sbor  1928  sban  1929  sbco3  1948  nfsbt  1950  elsb3  1952  elsb4  1953  sb9  1955  sbcom2v2  1962  sbcom2  1963  dfsb7  1967  sbid2v  1972  sbelx  1973  sbal  1976  sbal1  1978  sbex  1980  exsb  1984  dvelimALT  1986  dvelim  1993  dvelimor  1994  dveel1  1996  dveel2  1997  euf  2005  sb8euh  2023  euorv  2027  euex  2030  euanv  2057  mo4f  2060  moim  2064  moimv  2066  moanim  2074  mopick  2078  2eu4  2093  cleqh  2240  abeq2  2249  mpteq12  4019  bj-ex  13140  bj-inex  13276