Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-17 | Unicode version |
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.) |
Ref | Expression |
---|---|
ax-17 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . 2 | |
2 | vx | . . 3 | |
3 | 1, 2 | wal 1351 | . 2 |
4 | 1, 3 | wi 4 | 1 |
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 |