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

Axiom ax-17 1392
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
Distinct variable group:   ,

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2
2 vx . . 3  setvar
31, 2wal 1221 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a17d  1393  nfv  1394  exlimiv  1462  equid  1562  ax16  1667  dvelimfALT2  1671  exlimdv  1673  ax11a2  1675  albidv  1678  exbidv  1679  ax11v  1681  ax11ev  1682  ax16i  1711  ax16ALT  1712  equvin  1716  19.9v  1724  19.21v  1726  alrimiv  1727  alrimdv  1729  alimdv  1732  eximdv  1733  19.23v  1736  pm11.53  1748  19.27v  1752  19.28v  1753  19.41v  1755  19.42v  1759  cbvalv  1767  cbvexv  1768  cbvexdh  1774  nexdv  1784  cleljust  1786  sbhb  1789  hbsbv  1790  sbco2v  1794  nfsb  1795  equsb3lem  1797  equsb3  1798  sbn  1799  sbim  1800  sbor  1801  sban  1802  sbco3  1821  nfsbt  1823  elsb3  1825  elsb4  1826  sb9  1828  sbcom2v2  1835  sbcom2  1836  dfsb7  1840  sbid2v  1845  sbelx  1846  sbal  1849  sbal1  1851  sbex  1853  exsb  1857  dvelimALT  1859  dvelim  1866  dvelimor  1867  dveel1  1869  dveel2  1870  euf  1878  sb8euh  1896  euorv  1900  euex  1903  euanv  1930  mo4f  1933  moim  1937  moimv  1939  moanim  1947  mopick  1951  2eu4  1966  cleqh  2110  abeq2  2119  mpteq12  3803  bj-ex  8167  bj-inex  8288
  Copyright terms: Public domain W3C validator