Axiom ax-17 1550

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

This axiom is referenced by:  a17d  1551  nfv  1552  exlimiv  1622  equid  1725  ax16  1837  dvelimfALT2  1841  exlimdv  1843  ax11a2  1845  albidv  1848  exbidv  1849  ax11v  1851  ax11ev  1852  ax16i  1882  ax16ALT  1883  equvin  1887  19.9v  1895  19.21v  1897  alrimiv  1898  alrimdv  1900  alimdv  1903  eximdv  1904  19.23v  1907  pm11.53  1920  19.27v  1924  19.28v  1925  19.41v  1927  19.42v  1931  cbvalv  1942  cbvexv  1943  cbvexdh  1951  nexdv  1965  sbhb  1969  hbsbv  1970  sbco2vh  1974  nfsb  1975  equsb3lem  1979  equsb3  1980  sbn  1981  sbim  1982  sbor  1983  sban  1984  sbco3  2003  nfsbt  2005  sb9  2008  sbcom2v2  2015  sbcom2  2016  dfsb7  2020  sbid2v  2025  sbelx  2026  sbal  2029  sbal1  2031  sbex  2033  exsb  2037  dvelimALT  2039  dvelim  2046  dvelimor  2047  euf  2060  sb8euh  2078  euorv  2082  euex  2085  euanv  2113  mo4f  2116  moim  2120  moimv  2122  moanim  2130  mopick  2134  2eu4  2149  cleljust  2184  elsb1  2185  elsb2  2186  dveel1  2187  dveel2  2188  cleqh  2307  abeq2  2316  mpteq12  4143  bj-ex  15898  bj-inex  16042