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

Axiom ax-17 1349
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 1269, ax-4 1333 through ax-9 1354, ax-10o 1489, and ax-12 1335 through ax-16 1570: in that system, we can derive any instance of ax-17 1349 not containing wff variables by induction on formula length, using ax17eq 1938 and ax17el 1940 for the basis together hbn 1445, hbal 1296, and hbim 1368. 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 1266 . 2 wff xφ
41, 3wi 4 1 wff (φxφ)
Colors of variables: wff set class
This axiom is referenced by:  a17d  1350  nfv  1351  exlimiv  1408  equid  1475  a4imv  1567  ax16  1569  dvelimfALT2  1573  exlimdv  1575  ax11a2  1577  albidv  1580  exbidv  1581  ax11v  1583  ax11ev  1584  ax16i  1610  ax16ALT  1611  a4imev  1613  equvin  1615  19.9v  1623  19.21v  1624  alrimiv  1625  alrimdv  1627  alimdv  1630  eximdv  1631  19.23v  1634  pm11.53  1646  19.27v  1649  19.28v  1650  19.36aiv  1651  19.41v  1652  19.42v  1656  cbvalv  1663  cbvexv  1664  cbval2  1665  cbvex2  1666  cbval2v  1667  cbvex2v  1668  cbvald  1669  cbvexd  1670  eeanv  1673  nexdv  1676  cleljust  1678  sbhb  1681  sbhb2  1682  hbsbv  1683  sbco2v  1686  nfsb  1687  equsb3lem  1689  equsb3  1690  sbn  1691  sbim  1692  sbor  1693  sban  1694  sbco3  1712  elsb3  1714  elsb4  1715  sb9  1717  sbcom2v2  1723  sbcom2  1724  dfsb7  1729  sbid2v  1734  sbelx  1735  sbalyz  1737  sbal  1738  sbal1  1740  sbexyz  1741  sbex  1742  exsb  1744  dvelimALT  1746  dvelim  1752  dveel1  1754  dveel2  1755  19.37v  1765  eujustALT  1769  euf  1772  eubidv  1774  hbeud  1778  sb8eu  1779  mo  1782  euex  1783  euorv  1788  sbmo  1790  mo4f  1792  mo4  1793  eu5  1799  immo  1807  moimv  1809  moanim  1817  moanimv  1819  euanv  1822  mopick  1823  moexexv  1831  2mo  1839  2mos  1840  2eu4  1844  2eu6  1846  19.36v  1871  19.12vv  1874  ax4  1915  ax15  1916  ax11el  1921  a12study2  1936
  Copyright terms: Public domain W3C validator