![]() |
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 | ⊢ (φ → ∀xφ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . 2 wff φ | |
2 | vx | . . 3 setvar x | |
3 | 1, 2 | wal 1240 | . 2 wff ∀xφ |
4 | 1, 3 | wi 4 | 1 wff (φ → ∀xφ) |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1417 nfv 1418 exlimiv 1486 equid 1586 ax16 1691 dvelimfALT2 1695 exlimdv 1697 ax11a2 1699 albidv 1702 exbidv 1703 ax11v 1705 ax11ev 1706 ax16i 1735 ax16ALT 1736 equvin 1740 19.9v 1748 19.21v 1750 alrimiv 1751 alrimdv 1753 alimdv 1756 eximdv 1757 19.23v 1760 pm11.53 1772 19.27v 1776 19.28v 1777 19.41v 1779 19.42v 1783 cbvalv 1791 cbvexv 1792 cbvexdh 1798 nexdv 1808 cleljust 1810 sbhb 1813 hbsbv 1814 sbco2v 1818 nfsb 1819 equsb3lem 1821 equsb3 1822 sbn 1823 sbim 1824 sbor 1825 sban 1826 sbco3 1845 nfsbt 1847 elsb3 1849 elsb4 1850 sb9 1852 sbcom2v2 1859 sbcom2 1860 dfsb7 1864 sbid2v 1869 sbelx 1870 sbal 1873 sbal1 1875 sbex 1877 exsb 1881 dvelimALT 1883 dvelim 1890 dvelimor 1891 dveel1 1893 dveel2 1894 euf 1902 sb8euh 1920 euorv 1924 euex 1927 euanv 1954 mo4f 1957 moim 1961 moimv 1963 moanim 1971 mopick 1975 2eu4 1990 cleqh 2134 abeq2 2143 mpteq12 3831 bj-ex 9237 bj-inex 9362 |
Copyright terms: Public domain | W3C validator |