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 1314 | . 2 wff ∀𝑥𝜑 |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1492 nfv 1493 exlimiv 1562 equid 1662 ax16 1769 dvelimfALT2 1773 exlimdv 1775 ax11a2 1777 albidv 1780 exbidv 1781 ax11v 1783 ax11ev 1784 ax16i 1814 ax16ALT 1815 equvin 1819 19.9v 1827 19.21v 1829 alrimiv 1830 alrimdv 1832 alimdv 1835 eximdv 1836 19.23v 1839 pm11.53 1851 19.27v 1855 19.28v 1856 19.41v 1858 19.42v 1862 cbvalv 1871 cbvexv 1872 cbvexdh 1878 nexdv 1888 cleljust 1890 sbhb 1893 hbsbv 1894 sbco2v 1898 nfsb 1899 equsb3lem 1901 equsb3 1902 sbn 1903 sbim 1904 sbor 1905 sban 1906 sbco3 1925 nfsbt 1927 elsb3 1929 elsb4 1930 sb9 1932 sbcom2v2 1939 sbcom2 1940 dfsb7 1944 sbid2v 1949 sbelx 1950 sbal 1953 sbal1 1955 sbex 1957 exsb 1961 dvelimALT 1963 dvelim 1970 dvelimor 1971 dveel1 1973 dveel2 1974 euf 1982 sb8euh 2000 euorv 2004 euex 2007 euanv 2034 mo4f 2037 moim 2041 moimv 2043 moanim 2051 mopick 2055 2eu4 2070 cleqh 2217 abeq2 2226 mpteq12 3981 bj-ex 12865 bj-inex 13001 |
Copyright terms: Public domain | W3C validator |