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

Axiom ax-17 1491
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  |-  ( ph  ->  A. x ph )
Distinct variable group:    ph, x

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2  wff  ph
2 vx . . 3  setvar  x
31, 2wal 1314 . 2  wff  A. x ph
41, 3wi 4 1  wff  ( ph  ->  A. x ph )
Colors of variables: wff set class
This axiom is referenced by:  a17d  1492  nfv  1493  exlimiv  1562  equid  1662  ax16  1769  dvelimfALT2  1773  exlimdv  1775  ax11a2  1777  albidv  1780  exbidv  1781  ax11v  1783  ax11ev  1784  ax16i  1814  ax16ALT  1815  equvin  1819  19.9v  1827  19.21v  1829  alrimiv  1830  alrimdv  1832  alimdv  1835  eximdv  1836  19.23v  1839  pm11.53  1851  19.27v  1855  19.28v  1856  19.41v  1858  19.42v  1862  cbvalv  1871  cbvexv  1872  cbvexdh  1878  nexdv  1888  cleljust  1890  sbhb  1893  hbsbv  1894  sbco2v  1898  nfsb  1899  equsb3lem  1901  equsb3  1902  sbn  1903  sbim  1904  sbor  1905  sban  1906  sbco3  1925  nfsbt  1927  elsb3  1929  elsb4  1930  sb9  1932  sbcom2v2  1939  sbcom2  1940  dfsb7  1944  sbid2v  1949  sbelx  1950  sbal  1953  sbal1  1955  sbex  1957  exsb  1961  dvelimALT  1963  dvelim  1970  dvelimor  1971  dveel1  1973  dveel2  1974  euf  1982  sb8euh  2000  euorv  2004  euex  2007  euanv  2034  mo4f  2037  moim  2041  moimv  2043  moanim  2051  mopick  2055  2eu4  2070  cleqh  2217  abeq2  2226  mpteq12  3981  bj-ex  12865  bj-inex  13001
  Copyright terms: Public domain W3C validator