Axiom ax-17 1574

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	⊢ (𝜑 → ∀𝑥𝜑)

Distinct variable group:   𝜑,𝑥

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wal 1395	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  a17d  1575  nfv  1576  exlimiv  1646  equid  1749  ax16  1861  dvelimfALT2  1865  exlimdv  1867  ax11a2  1869  albidv  1872  exbidv  1873  ax11v  1875  ax11ev  1876  ax16i  1906  ax16ALT  1907  equvin  1911  19.9v  1919  19.21v  1921  alrimiv  1922  alrimdv  1924  alimdv  1927  eximdv  1928  19.23v  1931  pm11.53  1944  19.27v  1948  19.28v  1949  19.41v  1951  19.42v  1955  cbvalv  1966  cbvexv  1967  cbvexdh  1975  nexdv  1989  sbhb  1993  hbsbv  1994  sbco2vh  1998  nfsb  1999  equsb3lem  2003  equsb3  2004  sbn  2005  sbim  2006  sbor  2007  sban  2008  sbco3  2027  nfsbt  2029  sb9  2032  sbcom2v2  2039  sbcom2  2040  dfsb7  2044  sbid2v  2049  sbelx  2050  sbal  2053  sbal1  2055  sbex  2057  exsb  2061  dvelimALT  2063  dvelim  2070  dvelimor  2071  euf  2084  sb8euh  2102  euorv  2106  euex  2109  euanv  2137  mo4f  2140  moim  2144  moimv  2146  moanim  2154  mopick  2158  2eu4  2173  cleljust  2208  elsb1  2209  elsb2  2210  dveel1  2211  dveel2  2212  cleqh  2331  abeq2  2340  mpteq12  4172  bj-ex  16358  bj-inex  16502