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 1241 | . 2 |
4 | 1, 3 | wi 4 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1420 nfv 1421 exlimiv 1489 equid 1589 ax16 1694 dvelimfALT2 1698 exlimdv 1700 ax11a2 1702 albidv 1705 exbidv 1706 ax11v 1708 ax11ev 1709 ax16i 1738 ax16ALT 1739 equvin 1743 19.9v 1751 19.21v 1753 alrimiv 1754 alrimdv 1756 alimdv 1759 eximdv 1760 19.23v 1763 pm11.53 1775 19.27v 1779 19.28v 1780 19.41v 1782 19.42v 1786 cbvalv 1794 cbvexv 1795 cbvexdh 1801 nexdv 1811 cleljust 1813 sbhb 1816 hbsbv 1817 sbco2v 1821 nfsb 1822 equsb3lem 1824 equsb3 1825 sbn 1826 sbim 1827 sbor 1828 sban 1829 sbco3 1848 nfsbt 1850 elsb3 1852 elsb4 1853 sb9 1855 sbcom2v2 1862 sbcom2 1863 dfsb7 1867 sbid2v 1872 sbelx 1873 sbal 1876 sbal1 1878 sbex 1880 exsb 1884 dvelimALT 1886 dvelim 1893 dvelimor 1894 dveel1 1896 dveel2 1897 euf 1905 sb8euh 1923 euorv 1927 euex 1930 euanv 1957 mo4f 1960 moim 1964 moimv 1966 moanim 1974 mopick 1978 2eu4 1993 cleqh 2137 abeq2 2146 mpteq12 3840 bj-ex 9902 bj-inex 10027 |
Copyright terms: Public domain | W3C validator |