Axiom ax-17 1572

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 1393	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  a17d  1573  nfv  1574  exlimiv  1644  equid  1747  ax16  1859  dvelimfALT2  1863  exlimdv  1865  ax11a2  1867  albidv  1870  exbidv  1871  ax11v  1873  ax11ev  1874  ax16i  1904  ax16ALT  1905  equvin  1909  19.9v  1917  19.21v  1919  alrimiv  1920  alrimdv  1922  alimdv  1925  eximdv  1926  19.23v  1929  pm11.53  1942  19.27v  1946  19.28v  1947  19.41v  1949  19.42v  1953  cbvalv  1964  cbvexv  1965  cbvexdh  1973  nexdv  1987  sbhb  1991  hbsbv  1992  sbco2vh  1996  nfsb  1997  equsb3lem  2001  equsb3  2002  sbn  2003  sbim  2004  sbor  2005  sban  2006  sbco3  2025  nfsbt  2027  sb9  2030  sbcom2v2  2037  sbcom2  2038  dfsb7  2042  sbid2v  2047  sbelx  2048  sbal  2051  sbal1  2053  sbex  2055  exsb  2059  dvelimALT  2061  dvelim  2068  dvelimor  2069  euf  2082  sb8euh  2100  euorv  2104  euex  2107  euanv  2135  mo4f  2138  moim  2142  moimv  2144  moanim  2152  mopick  2156  2eu4  2171  cleljust  2206  elsb1  2207  elsb2  2208  dveel1  2209  dveel2  2210  cleqh  2329  abeq2  2338  mpteq12  4166  bj-ex  16084  bj-inex  16228