Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-17 GIF version

Axiom ax-17 1331
 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 1253, ax-4 1316 through ax-9 1336, ax-10o 1471, and ax-12 1318 through ax-16 1553: in that system, we can derive any instance of ax-17 1331 not containing wff variables by induction on formula length, using ax17eq 1915 and ax17el 1917 for the basis together hbn 1427, hbal 1280, and hbim 1350. 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). (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-17 (φxφ)
Distinct variable group:   φ,x

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2 wff φ
2 vx . . 3 set x
31, 2wal 1250 . 2 wff xφ
41, 3wi 4 1 wff (φxφ)
 Colors of variables: wff set class This axiom is referenced by:  a17d  1332  nfv  1333  exlimiv  1390  equid  1457  a4imv  1550  ax16  1552  dvelimfALT2  1556  exlimdv  1558  ax11a2  1560  albidv  1563  exbidv  1564  ax11v  1566  ax11ev  1567  ax16i  1598  ax16ALT  1599  a4imev  1601  equvin  1603  19.9v  1611  19.21v  1612  alrimiv  1613  alrimdv  1615  alimdv  1618  eximdv  1619  19.23v  1622  pm11.53  1634  19.27v  1637  19.28v  1638  19.36aiv  1639  19.41v  1640  19.42v  1644  cbvalv  1651  cbvexv  1652  cbval2  1653  cbvex2  1654  cbval2v  1655  cbvex2v  1656  cbvald  1657  cbvexd  1658  eeanv  1661  nexdv  1664  cleljust  1666  sbhb  1669  sbhb2  1670  hbsbv  1672  sbco2v  1674  equsb3lem  1675  equsb3  1676  sbn  1677  sbim  1678  sbor  1679  sban  1680  elsb3  1695  elsb4  1696  sbcom2v2  1704  sbcom2  1705  dfsb7  1710  sbid2v  1715  sbelx  1716  sbalyz  1718  sbal  1719  sbal1  1721  sbexyz  1722  sbex  1723  exsb  1725  dvelim  1727  dvelimALT  1728  dveel1  1731  dveel2  1732  19.37v  1741  eujustALT  1745  euf  1748  eubidv  1750  hbeud  1754  sb8eu  1755  mo  1758  euex  1759  euorv  1764  sbmo  1766  mo4f  1768  mo4  1769  eu5  1775  immo  1783  moimv  1785  moanim  1793  moanimv  1795  euanv  1798  mopick  1799  moexexv  1807  2mo  1815  2mos  1816  2eu4  1820  2eu6  1822  19.36v  1847  19.12vv  1850  ax4  1892  ax15  1893  ax11el  1898  a12study2  1913
 Copyright terms: Public domain W3C validator