![]() |
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 1362 | . 2 wff ∀𝑥𝜑 |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1538 nfv 1539 exlimiv 1609 equid 1712 ax16 1824 dvelimfALT2 1828 exlimdv 1830 ax11a2 1832 albidv 1835 exbidv 1836 ax11v 1838 ax11ev 1839 ax16i 1869 ax16ALT 1870 equvin 1874 19.9v 1882 19.21v 1884 alrimiv 1885 alrimdv 1887 alimdv 1890 eximdv 1891 19.23v 1894 pm11.53 1907 19.27v 1911 19.28v 1912 19.41v 1914 19.42v 1918 cbvalv 1929 cbvexv 1930 cbvexdh 1938 nexdv 1948 sbhb 1952 hbsbv 1953 sbco2vh 1957 nfsb 1958 equsb3lem 1962 equsb3 1963 sbn 1964 sbim 1965 sbor 1966 sban 1967 sbco3 1986 nfsbt 1988 sb9 1991 sbcom2v2 1998 sbcom2 1999 dfsb7 2003 sbid2v 2008 sbelx 2009 sbal 2012 sbal1 2014 sbex 2016 exsb 2020 dvelimALT 2022 dvelim 2029 dvelimor 2030 euf 2043 sb8euh 2061 euorv 2065 euex 2068 euanv 2095 mo4f 2098 moim 2102 moimv 2104 moanim 2112 mopick 2116 2eu4 2131 cleljust 2166 elsb1 2167 elsb2 2168 dveel1 2169 dveel2 2170 cleqh 2289 abeq2 2298 mpteq12 4101 bj-ex 14951 bj-inex 15096 |
Copyright terms: Public domain | W3C validator |