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

Axiom ax-17 1319
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 1257, ax-4 1310 through ax-9 1322, ax-10o 1455, and ax-12 1311 through ax-16 1523: in that system, we can derive any instance of ax-17 1319 not containing wff variables by induction on formula length, using ax17eq 1524 and ax17el 1687 for the basis together hbn 1341, hbal 1275, and hbim 1342. 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 1253 . 2 wff xφ
41, 3wi 4 1 wff (φxφ)
Colors of variables: wff set class
This axiom is referenced by:  a17d  1320  ax4  1326  equid1  1440  a4imv  1520  ax16  1522  dveeq2  1525  dvelimfALT2  1527  exlimdv  1529  ax11a2  1531  ax16i  1586  ax16ALT  1587  a4imev  1589  equvin  1591  albidv  1594  exbidv  1595  19.9v  1600  19.21v  1601  alrimiv  1602  alrimdv  1604  alimdv  1606  eximdv  1607  19.23v  1610  exlimiv  1612  pm11.53  1613  19.27v  1616  19.28v  1617  19.36v  1618  19.36aiv  1619  19.12vv  1620  19.37v  1621  19.41v  1623  19.42v  1627  cbvalv  1634  cbvexv  1635  cbval2  1636  cbvex2  1637  cbval2v  1638  cbvex2v  1639  cbvald  1640  eeanv  1644  nexdv  1647  cleljust  1649  equsb3lem  1650  equsb3  1651  elsb3  1652  elsb4  1653  sbhb  1655  sbhb2  1656  dfsb7  1666  sbid2v  1669  exsb  1676  dvelim  1678  dvelimALT  1679  dveeq1  1680  dveel1  1682  dveel2  1683  ax15  1685  eujustALT  1693  euf  1696  eubidv  1698  hbeud  1702  sb8eu  1703  mo  1706  euex  1707  euorv  1712  sbmo  1714  mo4f  1716  mo4  1717  eu5  1723  immo  1731  moimv  1733  moanim  1741  moanimv  1743  euanv  1746  mopick  1747  moexexv  1755  2mo  1763  2mos  1764  2eu4  1768  2eu6  1770  ax11el  1787  a12study2  1802
  Copyright terms: Public domain W3C validator