Axiom ax-17 1513

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

This axiom is referenced by:  a17d  1514  nfv  1515  exlimiv  1585  equid  1688  ax16  1800  dvelimfALT2  1804  exlimdv  1806  ax11a2  1808  albidv  1811  exbidv  1812  ax11v  1814  ax11ev  1815  ax16i  1845  ax16ALT  1846  equvin  1850  19.9v  1858  19.21v  1860  alrimiv  1861  alrimdv  1863  alimdv  1866  eximdv  1867  19.23v  1870  pm11.53  1882  19.27v  1886  19.28v  1887  19.41v  1889  19.42v  1893  cbvalv  1904  cbvexv  1905  cbvexdh  1913  nexdv  1923  sbhb  1927  hbsbv  1928  sbco2vh  1932  nfsb  1933  equsb3lem  1937  equsb3  1938  sbn  1939  sbim  1940  sbor  1941  sban  1942  sbco3  1961  nfsbt  1963  sb9  1966  sbcom2v2  1973  sbcom2  1974  dfsb7  1978  sbid2v  1983  sbelx  1984  sbal  1987  sbal1  1989  sbex  1991  exsb  1995  dvelimALT  1997  dvelim  2004  dvelimor  2005  euf  2018  sb8euh  2036  euorv  2040  euex  2043  euanv  2070  mo4f  2073  moim  2077  moimv  2079  moanim  2087  mopick  2091  2eu4  2106  cleljust  2141  elsb3  2142  elsb4  2143  dveel1  2144  dveel2  2145  cleqh  2264  abeq2  2273  mpteq12  4059  bj-ex  13478  bj-inex  13624