Axiom ax-17 1459

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

This axiom is referenced by:  a17d  1460  nfv  1461  exlimiv  1529  equid  1629  ax16  1734  dvelimfALT2  1738  exlimdv  1740  ax11a2  1742  albidv  1745  exbidv  1746  ax11v  1748  ax11ev  1749  ax16i  1779  ax16ALT  1780  equvin  1784  19.9v  1792  19.21v  1794  alrimiv  1795  alrimdv  1797  alimdv  1800  eximdv  1801  19.23v  1804  pm11.53  1816  19.27v  1820  19.28v  1821  19.41v  1823  19.42v  1827  cbvalv  1835  cbvexv  1836  cbvexdh  1842  nexdv  1852  cleljust  1854  sbhb  1857  hbsbv  1858  sbco2v  1862  nfsb  1863  equsb3lem  1865  equsb3  1866  sbn  1867  sbim  1868  sbor  1869  sban  1870  sbco3  1889  nfsbt  1891  elsb3  1893  elsb4  1894  sb9  1896  sbcom2v2  1903  sbcom2  1904  dfsb7  1908  sbid2v  1913  sbelx  1914  sbal  1917  sbal1  1919  sbex  1921  exsb  1925  dvelimALT  1927  dvelim  1934  dvelimor  1935  dveel1  1937  dveel2  1938  euf  1946  sb8euh  1964  euorv  1968  euex  1971  euanv  1998  mo4f  2001  moim  2005  moimv  2007  moanim  2015  mopick  2019  2eu4  2034  cleqh  2178  abeq2  2187  mpteq12  3861  bj-ex  10573  bj-inex  10698