Axiom ax-17 1402

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.

This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1339, ax-4 1392 through ax-9 1418, ax-10o 1576, and ax-12 1393 through ax-16 1644: in that system, we can derive any instance of ax-17 1402 not containing wff variables by induction on formula length, using ax17eq 1645 and ax17el 1808 for the basis together hbn 1438, hbal 1357, and hbim 1439. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct).

Assertion

Ref	Expression
ax-17	|- (ph -> A.xph)

Distinct variable group:   ph,x

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. . 3 set x
3	1, 2	wal 1335	. 2 wff A.xph
4	1, 3	wi 4	1 wff (ph -> A.xph)

This axiom is referenced by:  a17d  1403  a9wa9lem1  1404  a9wa9lem3  1407  a9wa9lem8  1413  a9wa9lem8OLD  1414  a9wa9  1415  a9wa9OLD  1416  ax4  1423  equid1  1561  a4imv  1641  ax16  1643  dveeq2  1646  dvelimfALT2  1648  exlimdv  1650  ax11a2  1652  ax16i  1707  ax16ALT  1708  a4imev  1710  equvin  1712  albidv  1715  exbidv  1716  19.9v  1721  19.21v  1722  alrimiv  1723  alrimdv  1725  alimdv  1727  eximdv  1728  19.23v  1731  exlimiv  1733  pm11.53  1734  19.27v  1737  19.28v  1738  19.36v  1739  19.36aiv  1740  19.12vv  1741  19.37v  1742  19.41v  1744  19.42v  1748  cbvalv  1755  cbvexv  1756  cbval2  1757  cbvex2  1758  cbval2v  1759  cbvex2v  1760  cbvald  1761  eeanv  1765  nexdv  1768  cleljust  1770  equsb3lem  1771  equsb3  1772  elsb3  1773  elsb4  1774  sbhb  1776  sbhb2  1777  dfsb7  1787  sbid2v  1790  exsb  1797  dvelim  1799  dvelimALT  1800  dveeq1  1801  dveel1  1803  dveel2  1804  ax15  1806  ax11el  1811  a12study2  1827  eujustALT  1832  euf  1835  eubidv  1837  hbeud  1841  sb8eu  1842  mo  1845  euex  1846  euorv  1851  sbmo  1853  mo4f  1855  mo4  1856  eu5  1862  immo  1870  moimv  1872  moanim  1880  moanimv  1882  euanv  1885  mopick  1886  moexexv  1894  2mo  1902  2mos  1903  2eu4  1907  2eu6  1909