Axiom ax-17 1540

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

This axiom is referenced by:  a17d  1541  nfv  1542  exlimiv  1612  equid  1715  ax16  1827  dvelimfALT2  1831  exlimdv  1833  ax11a2  1835  albidv  1838  exbidv  1839  ax11v  1841  ax11ev  1842  ax16i  1872  ax16ALT  1873  equvin  1877  19.9v  1885  19.21v  1887  alrimiv  1888  alrimdv  1890  alimdv  1893  eximdv  1894  19.23v  1897  pm11.53  1910  19.27v  1914  19.28v  1915  19.41v  1917  19.42v  1921  cbvalv  1932  cbvexv  1933  cbvexdh  1941  nexdv  1955  sbhb  1959  hbsbv  1960  sbco2vh  1964  nfsb  1965  equsb3lem  1969  equsb3  1970  sbn  1971  sbim  1972  sbor  1973  sban  1974  sbco3  1993  nfsbt  1995  sb9  1998  sbcom2v2  2005  sbcom2  2006  dfsb7  2010  sbid2v  2015  sbelx  2016  sbal  2019  sbal1  2021  sbex  2023  exsb  2027  dvelimALT  2029  dvelim  2036  dvelimor  2037  euf  2050  sb8euh  2068  euorv  2072  euex  2075  euanv  2102  mo4f  2105  moim  2109  moimv  2111  moanim  2119  mopick  2123  2eu4  2138  cleljust  2173  elsb1  2174  elsb2  2175  dveel1  2176  dveel2  2177  cleqh  2296  abeq2  2305  mpteq12  4116  bj-ex  15408  bj-inex  15553