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

Axiom ax-17 1297
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 1235, ax-4 1288 through ax-9 1300, ax-10o 1427, and ax-12 1289 through ax-16 1502: in that system, we can derive any instance of ax-17 1297 not containing wff variables by induction on formula length, using ax17eq 1503 and ax17el 1682 for the basis together hbn 1318, hbal 1253, and hbim 1319. 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 1231 . 2 wff xφ
41, 3wi 4 1 wff (φxφ)
Colors of variables: wff set class
This axiom is referenced by:  a17d  1298  equid  1413  a4imv  1499  ax16  1501  dveeq2  1504  dvelimfALT2  1506  exlimdv  1508  ax11a2  1510  ax16i  1563  ax16ALT  1564  a4imev  1566  equvin  1568  albidv  1571  exbidv  1572  19.9v  1577  19.21v  1578  alrimiv  1579  alrimdv  1581  alimdv  1583  eximdv  1584  19.23v  1587  exlimiv  1589  ax11v  1590  pm11.53  1599  19.27v  1602  19.28v  1603  19.36aiv  1604  19.37v  1605  19.41v  1607  19.42v  1611  cbvalv  1618  cbvexv  1619  cbval2  1620  cbvex2  1621  cbval2v  1622  cbvex2v  1623  cbvald  1624  cbvexd  1625  eeanv  1628  nexdv  1631  cleljust  1633  equsb3lem  1634  equsb3  1635  elsb3  1636  elsb4  1637  sbhb  1640  sbhb2  1641  hbsbv  1647  dfsb7  1659  sbid2v  1662  sbelx  1663  sbalyz  1667  sbexyz  1669  exsb  1671  dvelim  1673  dvelimALT  1674  dveeq1  1675  dveel1  1677  dveel2  1678  ax15  1680  eujustALT  1691  euf  1694  eubidv  1696  hbeud  1700  sb8eu  1701  mo  1704  euex  1705  euorv  1710  sbmo  1712  mo4f  1714  mo4  1715  eu5  1721  immo  1729  moimv  1731  moanim  1739  moanimv  1741  euanv  1744  mopick  1745  moexexv  1753  2mo  1761  2mos  1762  2eu4  1766  2eu6  1768  19.36v  1797  19.12vv  1798  ax4  1809  ax11el  1812  a12study2  1827
  Copyright terms: Public domain W3C validator