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

Axiom ax-17 1462
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 1285 . 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  1463  nfv  1464  exlimiv  1532  equid  1632  ax16  1738  dvelimfALT2  1742  exlimdv  1744  ax11a2  1746  albidv  1749  exbidv  1750  ax11v  1752  ax11ev  1753  ax16i  1783  ax16ALT  1784  equvin  1788  19.9v  1796  19.21v  1798  alrimiv  1799  alrimdv  1801  alimdv  1804  eximdv  1805  19.23v  1808  pm11.53  1820  19.27v  1824  19.28v  1825  19.41v  1827  19.42v  1831  cbvalv  1839  cbvexv  1840  cbvexdh  1846  nexdv  1856  cleljust  1858  sbhb  1861  hbsbv  1862  sbco2v  1866  nfsb  1867  equsb3lem  1869  equsb3  1870  sbn  1871  sbim  1872  sbor  1873  sban  1874  sbco3  1893  nfsbt  1895  elsb3  1897  elsb4  1898  sb9  1900  sbcom2v2  1907  sbcom2  1908  dfsb7  1912  sbid2v  1917  sbelx  1918  sbal  1921  sbal1  1923  sbex  1925  exsb  1929  dvelimALT  1931  dvelim  1938  dvelimor  1939  dveel1  1941  dveel2  1942  euf  1950  sb8euh  1968  euorv  1972  euex  1975  euanv  2002  mo4f  2005  moim  2009  moimv  2011  moanim  2019  mopick  2023  2eu4  2038  cleqh  2184  abeq2  2193  mpteq12  3896  bj-ex  11108  bj-inex  11243
  Copyright terms: Public domain W3C validator