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

Axiom ax-17 1280
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 1218, ax-4 1271 through ax-9 1283, ax-10o 1406, and ax-12 1272 through ax-16 1481: in that system, we can derive any instance of ax-17 1280 not containing wff variables by induction on formula length, using ax17eq 1482 and ax17el 1661 for the basis together hbn 1301, hbal 1236, and hbim 1302. 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
Distinct variable group:   ,

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2
2 vx . . 3
31, 2wal 1214 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a17d  1281  equid  1392  a4imv  1478  ax16  1480  dveeq2  1483  dvelimfALT2  1485  exlimdv  1487  ax11a2  1489  ax16i  1542  ax16ALT  1543  a4imev  1545  equvin  1547  albidv  1550  exbidv  1551  19.9v  1556  19.21v  1557  alrimiv  1558  alrimdv  1560  alimdv  1562  eximdv  1563  19.23v  1566  exlimiv  1568  ax11v  1569  ax11ev  1570  pm11.53  1579  19.27v  1582  19.28v  1583  19.36aiv  1584  19.41v  1585  19.42v  1589  cbvalv  1596  cbvexv  1597  cbval2  1598  cbvex2  1599  cbval2v  1600  cbvex2v  1601  cbvald  1602  cbvexd  1603  eeanv  1606  nexdv  1609  cleljust  1611  equsb3lem  1612  equsb3  1613  elsb3  1614  elsb4  1615  sbco2iv  1618  sbhb  1619  sbhb2  1620  hbsbv  1626  dfsb7  1638  sbid2v  1641  sbelx  1642  sbalyz  1646  sbexyz  1648  exsb  1650  dvelim  1652  dvelimALT  1653  dveeq1  1654  dveel1  1656  dveel2  1657  ax15  1659  19.37v  1668  eujustALT  1672  euf  1675  eubidv  1677  hbeud  1681  sb8eu  1682  mo  1685  euex  1686  euorv  1691  sbmo  1693  mo4f  1695  mo4  1696  eu5  1702  immo  1710  moimv  1712  moanim  1720  moanimv  1722  euanv  1725  mopick  1726  moexexv  1734  2mo  1742  2mos  1743  2eu4  1747  2eu6  1749  19.36v  1774  19.12vv  1776  ax4  1808  ax11el  1811  a12study2  1826
  Copyright terms: Public domain W3C validator