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

Axiom ax-17 1396
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 1224 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a17d  1397  nfv  1398  exlimiv  1467  equid  1567  ax16  1672  dvelimfALT2  1676  exlimdv  1678  ax11a2  1680  albidv  1683  exbidv  1684  ax11v  1686  ax11ev  1687  ax16i  1716  ax16ALT  1717  equvin  1721  19.9v  1729  19.21v  1731  alrimiv  1732  alrimdv  1734  alimdv  1737  eximdv  1738  19.23v  1741  pm11.53  1753  19.27v  1757  19.28v  1758  19.41v  1760  19.42v  1764  cbvalv  1772  cbvexv  1773  cbvexdh  1779  nexdv  1789  cleljust  1791  sbhb  1794  hbsbv  1795  sbco2v  1799  nfsb  1800  equsb3lem  1802  equsb3  1803  sbn  1804  sbim  1805  sbor  1806  sban  1807  sbco3  1826  nfsbt  1828  elsb3  1830  elsb4  1831  sb9  1833  sbcom2v2  1840  sbcom2  1841  dfsb7  1845  sbid2v  1850  sbelx  1851  sbal  1854  sbal1  1856  sbex  1858  exsb  1862  dvelimALT  1864  dvelim  1871  dvelimor  1872  dveel1  1874  dveel2  1875  euf  1883  sb8euh  1901  euorv  1905  euex  1908  euanv  1935  mo4f  1938  moim  1942  moimv  1944  moanim  1952  mopick  1956  2eu4  1971  cleqh  2115  abeq2  2124  mpteq12  3810  bj-ex  7201  bj-inex  7322
  Copyright terms: Public domain W3C validator