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

Axiom ax-17 1419
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 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wal 1241 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff set class
This axiom is referenced by:  a17d  1420  nfv  1421  exlimiv  1489  equid  1589  ax16  1694  dvelimfALT2  1698  exlimdv  1700  ax11a2  1702  albidv  1705  exbidv  1706  ax11v  1708  ax11ev  1709  ax16i  1738  ax16ALT  1739  equvin  1743  19.9v  1751  19.21v  1753  alrimiv  1754  alrimdv  1756  alimdv  1759  eximdv  1760  19.23v  1763  pm11.53  1775  19.27v  1779  19.28v  1780  19.41v  1782  19.42v  1786  cbvalv  1794  cbvexv  1795  cbvexdh  1801  nexdv  1811  cleljust  1813  sbhb  1816  hbsbv  1817  sbco2v  1821  nfsb  1822  equsb3lem  1824  equsb3  1825  sbn  1826  sbim  1827  sbor  1828  sban  1829  sbco3  1848  nfsbt  1850  elsb3  1852  elsb4  1853  sb9  1855  sbcom2v2  1862  sbcom2  1863  dfsb7  1867  sbid2v  1872  sbelx  1873  sbal  1876  sbal1  1878  sbex  1880  exsb  1884  dvelimALT  1886  dvelim  1893  dvelimor  1894  dveel1  1896  dveel2  1897  euf  1905  sb8euh  1923  euorv  1927  euex  1930  euanv  1957  mo4f  1960  moim  1964  moimv  1966  moanim  1974  mopick  1978  2eu4  1993  cleqh  2137  abeq2  2146  mpteq12  3837  bj-ex  9766  bj-inex  9891
  Copyright terms: Public domain W3C validator