Axiom ax-17 1357

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	⊢ (φ → ∀xφ)

Distinct variable group:   φ,x

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff φ
2		vx	. . 3 set x
3	1, 2	wal 1272	. 2 wff ∀xφ
4	1, 3	wi 4	1 wff (φ → ∀xφ)

This axiom is referenced by:  a17d  1358  nfv  1359  exlimiv  1425  equid  1511  ax16  1615  dvelimfALT2  1619  exlimdv  1621  ax11a2  1623  albidv  1626  exbidv  1627  ax11v  1629  ax11ev  1630  ax16i  1659  ax16ALT  1660  equvin  1664  19.9v  1672  19.21v  1673  alrimiv  1674  alrimdv  1676  alimdv  1679  eximdv  1680  19.23v  1683  pm11.53  1695  19.27v  1698  19.28v  1699  19.41v  1701  19.42v  1705  cbvalv  1712  cbvexv  1713  cbval2  1714  cbvex2  1715  cbval2v  1716  cbvex2v  1717  cbvexdh  1719  nexdv  1728  cleljust  1730  sbhb  1733  hbsbv  1734  sbco2v  1738  nfsb  1739  equsb3lem  1741  equsb3  1742  sbn  1743  sbim  1744  sbor  1745  sban  1746  sbco3  1765  nfsbt  1767  elsb3  1769  elsb4  1770  sb9  1772  sbcom2v2  1779  sbcom2  1780  dfsb7  1784  sbid2v  1789  sbelx  1790  sbal  1793  sbal1  1795  sbex  1797  exsb  1799  dvelimALT  1801  dvelim  1808  dvelimor  1809  dveel1  1811  dveel2  1812  euf  1820  sb8euh  1836  euorv  1840  euex  1843  euanv  1869  mo4f  1872  moim  1876  moimv  1878  moanim  1886  mopick  1891  2eu4  1905  cleqh  2024  abeq2  2032  19.37v  2985  mo  2986  2mo  2992  2mos  2993  2eu6  2998  19.36v  3008  19.12vv  3011