Axiom ax-17 1575

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

This axiom is referenced by:  a17d  1576  nfv  1577  exlimiv  1647  equid  1749  equsexvw  1777  ax16  1862  dvelimfALT2  1866  exlimdv  1868  ax11a2  1870  albidv  1873  exbidv  1874  ax11v  1876  ax11ev  1877  ax16i  1907  ax16ALT  1908  equvin  1912  19.9v  1920  19.21v  1922  alrimiv  1923  alrimdv  1925  alimdv  1928  eximdv  1929  19.23v  1932  pm11.53  1945  19.27v  1949  19.28v  1950  19.41v  1952  19.42v  1956  cbvalv  1967  cbvexv  1968  cbvexdh  1976  nexdv  1990  sbhb  1994  hbsbv  1995  sbco2vh  1999  nfsb  2000  equsb3lem  2004  equsb3  2005  sbn  2006  sbim  2007  sbor  2008  sban  2009  sbco3  2028  nfsbt  2030  sb9  2033  sbcom2v2  2040  sbcom2  2041  dfsb7  2045  sbid2v  2050  sbelx  2051  sbal  2054  sbal1  2056  sbex  2058  exsb  2062  dvelimALT  2064  dvelim  2071  dvelimor  2072  euf  2085  sb8euh  2103  euorv  2107  euex  2110  euanv  2138  mo4f  2141  moim  2145  moimv  2147  moanim  2155  mopick  2159  2eu4  2174  cleljust  2209  elsb1  2210  elsb2  2211  dveel1  2212  dveel2  2213  cleqh  2332  abeq2  2341  mpteq12  4192  bj-ex  16521  bj-inex  16664