![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-17 | GIF 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 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | wal 1351 | . 2 wff ∀𝑥𝜑 |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1527 nfv 1528 exlimiv 1598 equid 1701 ax16 1813 dvelimfALT2 1817 exlimdv 1819 ax11a2 1821 albidv 1824 exbidv 1825 ax11v 1827 ax11ev 1828 ax16i 1858 ax16ALT 1859 equvin 1863 19.9v 1871 19.21v 1873 alrimiv 1874 alrimdv 1876 alimdv 1879 eximdv 1880 19.23v 1883 pm11.53 1895 19.27v 1899 19.28v 1900 19.41v 1902 19.42v 1906 cbvalv 1917 cbvexv 1918 cbvexdh 1926 nexdv 1936 sbhb 1940 hbsbv 1941 sbco2vh 1945 nfsb 1946 equsb3lem 1950 equsb3 1951 sbn 1952 sbim 1953 sbor 1954 sban 1955 sbco3 1974 nfsbt 1976 sb9 1979 sbcom2v2 1986 sbcom2 1987 dfsb7 1991 sbid2v 1996 sbelx 1997 sbal 2000 sbal1 2002 sbex 2004 exsb 2008 dvelimALT 2010 dvelim 2017 dvelimor 2018 euf 2031 sb8euh 2049 euorv 2053 euex 2056 euanv 2083 mo4f 2086 moim 2090 moimv 2092 moanim 2100 mopick 2104 2eu4 2119 cleljust 2154 elsb1 2155 elsb2 2156 dveel1 2157 dveel2 2158 cleqh 2277 abeq2 2286 mpteq12 4086 bj-ex 14484 bj-inex 14629 |
Copyright terms: Public domain | W3C validator |