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

Axiom ax-17 1524
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 1351 . 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  1525  nfv  1526  exlimiv  1596  equid  1699  ax16  1811  dvelimfALT2  1815  exlimdv  1817  ax11a2  1819  albidv  1822  exbidv  1823  ax11v  1825  ax11ev  1826  ax16i  1856  ax16ALT  1857  equvin  1861  19.9v  1869  19.21v  1871  alrimiv  1872  alrimdv  1874  alimdv  1877  eximdv  1878  19.23v  1881  pm11.53  1893  19.27v  1897  19.28v  1898  19.41v  1900  19.42v  1904  cbvalv  1915  cbvexv  1916  cbvexdh  1924  nexdv  1934  sbhb  1938  hbsbv  1939  sbco2vh  1943  nfsb  1944  equsb3lem  1948  equsb3  1949  sbn  1950  sbim  1951  sbor  1952  sban  1953  sbco3  1972  nfsbt  1974  sb9  1977  sbcom2v2  1984  sbcom2  1985  dfsb7  1989  sbid2v  1994  sbelx  1995  sbal  1998  sbal1  2000  sbex  2002  exsb  2006  dvelimALT  2008  dvelim  2015  dvelimor  2016  euf  2029  sb8euh  2047  euorv  2051  euex  2054  euanv  2081  mo4f  2084  moim  2088  moimv  2090  moanim  2098  mopick  2102  2eu4  2117  cleljust  2152  elsb1  2153  elsb2  2154  dveel1  2155  dveel2  2156  cleqh  2275  abeq2  2284  mpteq12  4081  bj-ex  14054  bj-inex  14199
  Copyright terms: Public domain W3C validator