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

Axiom ax-17 1352
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.

(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 1267 . 2 wff xφ
41, 3wi 4 1 wff (φxφ)
Colors of variables: wff set class
This axiom is referenced by:  a17d  1353  nfv  1354  exlimiv  1420  equid  1503  a4imv  1602  ax16  1604  dvelimfALT2  1608  exlimdv  1610  ax11a2  1612  albidv  1615  exbidv  1616  ax11v  1618  ax11ev  1619  ax16i  1647  ax16ALT  1648  a4imev  1650  equvin  1652  19.9v  1660  19.21v  1661  alrimiv  1662  alrimdv  1664  alimdv  1667  eximdv  1668  19.23v  1671  pm11.53  1683  19.27v  1686  19.28v  1687  19.41v  1689  19.42v  1693  cbvalv  1700  cbvexv  1701  cbval2  1702  cbvex2  1703  cbval2v  1704  cbvex2v  1705  cbvexdh  1707  nexdv  1716  cleljust  1718  sbhb  1721  sbhb2  1722  hbsbv  1723  sbco2v  1727  nfsb  1728  equsb3lem  1730  equsb3  1731  sbn  1732  sbim  1733  sbor  1734  sban  1735  sbco3  1754  nfsbt  1756  elsb3  1758  elsb4  1759  sb9  1761  sbcom2v2  1767  sbcom2  1768  dfsb7  1773  sbid2v  1778  sbelx  1779  sbalyz  1781  sbal  1782  sbal1  1784  sbexyz  1785  sbex  1786  exsb  1788  dvelimALT  1790  dvelim  1797  dvelimor  1798  dveel1  1800  dveel2  1801  euf  1809  sb8euh  1825  euorv  1829  euex  1830  euanv  1845  cleqh  1964  abeq2  1972  19.37v  2547  mo  2548  sbmo  2552  mo4f  2554  mo4  2555  immo  2559  moimv  2561  moanim  2569  moanimv  2570  mopick  2573  moexexv  2580  2mo  2587  2mos  2588  2eu4  2592  2eu6  2594  19.36v  2608  19.12vv  2611
  Copyright terms: Public domain W3C validator