Axiom ax-17 1350

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 1266	. 2 wff ∀xφ
4	1, 3	wi 4	1 wff (φ → ∀xφ)

This axiom is referenced by:  a17d  1351  nfv  1352  exlimiv  1412  equid  1480  a4imv  1578  ax16  1580  dvelimfALT2  1584  exlimdv  1586  ax11a2  1588  albidv  1591  exbidv  1592  ax11v  1594  ax11ev  1595  ax16i  1621  ax16ALT  1622  a4imev  1624  equvin  1626  19.9v  1634  19.21v  1635  alrimiv  1636  alrimdv  1638  alimdv  1641  eximdv  1642  19.23v  1645  pm11.53  1657  19.27v  1660  19.28v  1661  19.36aiv  1662  19.41v  1663  19.42v  1667  cbvalv  1674  cbvexv  1675  cbval2  1676  cbvex2  1677  cbval2v  1678  cbvex2v  1679  cbvald  1680  cbvexd  1681  eeanv  1684  nexdv  1687  cleljust  1689  sbhb  1692  sbhb2  1693  hbsbv  1694  sbco2v  1698  nfsb  1699  equsb3lem  1701  equsb3  1702  sbn  1703  sbim  1704  sbor  1705  sban  1706  sbco3  1725  nfsbt  1727  elsb3  1729  elsb4  1730  sb9  1732  sbcom2v2  1738  sbcom2  1739  dfsb7  1744  sbid2v  1749  sbelx  1750  sbalyz  1752  sbal  1753  sbal1  1755  sbexyz  1756  sbex  1757  exsb  1759  dvelimALT  1761  dvelim  1768  dvelimor  1769  dveel1  1771  dveel2  1772  cleqh  1889  abeq2  1897  19.37v  2074  eujustALT  2078  euf  2081  eubidv  2083  hbeud  2087  sb8eu  2088  mo  2091  euex  2092  euorv  2097  sbmo  2099  mo4f  2101  mo4  2102  eu5  2108  immo  2116  moimv  2118  moanim  2126  moanimv  2128  euanv  2131  mopick  2132  moexexv  2140  2mo  2148  2mos  2149  2eu4  2153  2eu6  2155  19.36v  2171  19.12vv  2174