Axiom ax-17 1549

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  1550  nfv  1551  exlimiv  1621  equid  1724  ax16  1836  dvelimfALT2  1840  exlimdv  1842  ax11a2  1844  albidv  1847  exbidv  1848  ax11v  1850  ax11ev  1851  ax16i  1881  ax16ALT  1882  equvin  1886  19.9v  1894  19.21v  1896  alrimiv  1897  alrimdv  1899  alimdv  1902  eximdv  1903  19.23v  1906  pm11.53  1919  19.27v  1923  19.28v  1924  19.41v  1926  19.42v  1930  cbvalv  1941  cbvexv  1942  cbvexdh  1950  nexdv  1964  sbhb  1968  hbsbv  1969  sbco2vh  1973  nfsb  1974  equsb3lem  1978  equsb3  1979  sbn  1980  sbim  1981  sbor  1982  sban  1983  sbco3  2002  nfsbt  2004  sb9  2007  sbcom2v2  2014  sbcom2  2015  dfsb7  2019  sbid2v  2024  sbelx  2025  sbal  2028  sbal1  2030  sbex  2032  exsb  2036  dvelimALT  2038  dvelim  2045  dvelimor  2046  euf  2059  sb8euh  2077  euorv  2081  euex  2084  euanv  2111  mo4f  2114  moim  2118  moimv  2120  moanim  2128  mopick  2132  2eu4  2147  cleljust  2182  elsb1  2183  elsb2  2184  dveel1  2185  dveel2  2186  cleqh  2305  abeq2  2314  mpteq12  4127  bj-ex  15698  bj-inex  15843