Axiom ax-17 1514

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 1341	. 2 wff A. x ph
4	1, 3	wi 4	1 wff ( ph -> A. x ph )

This axiom is referenced by:  a17d  1515  nfv  1516  exlimiv  1586  equid  1689  ax16  1801  dvelimfALT2  1805  exlimdv  1807  ax11a2  1809  albidv  1812  exbidv  1813  ax11v  1815  ax11ev  1816  ax16i  1846  ax16ALT  1847  equvin  1851  19.9v  1859  19.21v  1861  alrimiv  1862  alrimdv  1864  alimdv  1867  eximdv  1868  19.23v  1871  pm11.53  1883  19.27v  1887  19.28v  1888  19.41v  1890  19.42v  1894  cbvalv  1905  cbvexv  1906  cbvexdh  1914  nexdv  1924  sbhb  1928  hbsbv  1929  sbco2vh  1933  nfsb  1934  equsb3lem  1938  equsb3  1939  sbn  1940  sbim  1941  sbor  1942  sban  1943  sbco3  1962  nfsbt  1964  sb9  1967  sbcom2v2  1974  sbcom2  1975  dfsb7  1979  sbid2v  1984  sbelx  1985  sbal  1988  sbal1  1990  sbex  1992  exsb  1996  dvelimALT  1998  dvelim  2005  dvelimor  2006  euf  2019  sb8euh  2037  euorv  2041  euex  2044  euanv  2071  mo4f  2074  moim  2078  moimv  2080  moanim  2088  mopick  2092  2eu4  2107  cleljust  2142  elsb1  2143  elsb2  2144  dveel1  2145  dveel2  2146  cleqh  2266  abeq2  2275  mpteq12  4065  bj-ex  13643  bj-inex  13789