![]() |
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 1283 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | wi 4 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1461 nfv 1462 exlimiv 1530 equid 1630 ax16 1736 dvelimfALT2 1740 exlimdv 1742 ax11a2 1744 albidv 1747 exbidv 1748 ax11v 1750 ax11ev 1751 ax16i 1781 ax16ALT 1782 equvin 1786 19.9v 1794 19.21v 1796 alrimiv 1797 alrimdv 1799 alimdv 1802 eximdv 1803 19.23v 1806 pm11.53 1818 19.27v 1822 19.28v 1823 19.41v 1825 19.42v 1829 cbvalv 1837 cbvexv 1838 cbvexdh 1844 nexdv 1854 cleljust 1856 sbhb 1859 hbsbv 1860 sbco2v 1864 nfsb 1865 equsb3lem 1867 equsb3 1868 sbn 1869 sbim 1870 sbor 1871 sban 1872 sbco3 1891 nfsbt 1893 elsb3 1895 elsb4 1896 sb9 1898 sbcom2v2 1905 sbcom2 1906 dfsb7 1910 sbid2v 1915 sbelx 1916 sbal 1919 sbal1 1921 sbex 1923 exsb 1927 dvelimALT 1929 dvelim 1936 dvelimor 1937 dveel1 1939 dveel2 1940 euf 1948 sb8euh 1966 euorv 1970 euex 1973 euanv 2000 mo4f 2003 moim 2007 moimv 2009 moanim 2017 mopick 2021 2eu4 2036 cleqh 2182 abeq2 2191 mpteq12 3882 bj-ex 10817 bj-inex 10949 |
Copyright terms: Public domain | W3C validator |