Axiom ax-17 1487

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	|- ( ph -> A. x ph )

Distinct variable group:   ph, x

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. . 3 setvar x
3	1, 2	wal 1310	. 2 wff A. x ph
4	1, 3	wi 4	1 wff ( ph -> A. x ph )

This axiom is referenced by:  a17d  1488  nfv  1489  exlimiv  1558  equid  1658  ax16  1765  dvelimfALT2  1769  exlimdv  1771  ax11a2  1773  albidv  1776  exbidv  1777  ax11v  1779  ax11ev  1780  ax16i  1810  ax16ALT  1811  equvin  1815  19.9v  1823  19.21v  1825  alrimiv  1826  alrimdv  1828  alimdv  1831  eximdv  1832  19.23v  1835  pm11.53  1847  19.27v  1851  19.28v  1852  19.41v  1854  19.42v  1858  cbvalv  1867  cbvexv  1868  cbvexdh  1874  nexdv  1884  cleljust  1886  sbhb  1889  hbsbv  1890  sbco2v  1894  nfsb  1895  equsb3lem  1897  equsb3  1898  sbn  1899  sbim  1900  sbor  1901  sban  1902  sbco3  1921  nfsbt  1923  elsb3  1925  elsb4  1926  sb9  1928  sbcom2v2  1935  sbcom2  1936  dfsb7  1940  sbid2v  1945  sbelx  1946  sbal  1949  sbal1  1951  sbex  1953  exsb  1957  dvelimALT  1959  dvelim  1966  dvelimor  1967  dveel1  1969  dveel2  1970  euf  1978  sb8euh  1996  euorv  2000  euex  2003  euanv  2030  mo4f  2033  moim  2037  moimv  2039  moanim  2047  mopick  2051  2eu4  2066  cleqh  2212  abeq2  2221  mpteq12  3969  bj-ex  12653  bj-inex  12788