Axiom ax-17 1435

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

This axiom is referenced by:  a17d  1436  nfv  1437  exlimiv  1505  equid  1605  ax16  1710  dvelimfALT2  1714  exlimdv  1716  ax11a2  1718  albidv  1721  exbidv  1722  ax11v  1724  ax11ev  1725  ax16i  1754  ax16ALT  1755  equvin  1759  19.9v  1767  19.21v  1769  alrimiv  1770  alrimdv  1772  alimdv  1775  eximdv  1776  19.23v  1779  pm11.53  1791  19.27v  1795  19.28v  1796  19.41v  1798  19.42v  1802  cbvalv  1810  cbvexv  1811  cbvexdh  1817  nexdv  1827  cleljust  1829  sbhb  1832  hbsbv  1833  sbco2v  1837  nfsb  1838  equsb3lem  1840  equsb3  1841  sbn  1842  sbim  1843  sbor  1844  sban  1845  sbco3  1864  nfsbt  1866  elsb3  1868  elsb4  1869  sb9  1871  sbcom2v2  1878  sbcom2  1879  dfsb7  1883  sbid2v  1888  sbelx  1889  sbal  1892  sbal1  1894  sbex  1896  exsb  1900  dvelimALT  1902  dvelim  1909  dvelimor  1910  dveel1  1912  dveel2  1913  euf  1921  sb8euh  1939  euorv  1943  euex  1946  euanv  1973  mo4f  1976  moim  1980  moimv  1982  moanim  1990  mopick  1994  2eu4  2009  cleqh  2153  abeq2  2162  mpteq12  3867  bj-ex  10268  bj-inex  10393