![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax6e | Structured version Visualization version Unicode version |
Description: At least one individual
exists. This is not a theorem of free logic,
which is sound in empty domains. For such a logic, we would add this
theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the
system consisting of ax-4 1682 through ax-9 1896,
all axioms other than
ax-6 1805 are believed to be theorems of free logic,
although the system
without ax-6 1805 is not complete in free logic.
It is preferred to use ax6ev 1807 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after axc9lem1 2093 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
Ref | Expression |
---|---|
ax6e |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 1935 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | axc9lem1 2093 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ax6ev 1807 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | equtr 1865 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eximii 1709 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | 19.35i 1741 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 6 | syl6com 36 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | ax6ev 1807 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | exlimiiv 1777 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 9 | pm2.61i 168 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-12 1933 ax-13 2091 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 |
This theorem is referenced by: ax6 2095 spimt 2097 spim 2098 spimed 2099 spimv 2101 spei 2105 equs4 2127 equsal 2128 equsexALT 2131 equvini 2179 equveli 2180 2ax6elem 2278 axi9 2427 dtrucor2 4634 axextnd 9016 ax8dfeq 30445 bj-alequex 31309 ax6er 31435 exlimiieq1 31436 wl-exeq 31867 wl-equsald 31872 ax6e2nd 36925 ax6e2ndVD 37305 ax6e2ndALT 37327 |
Copyright terms: Public domain | W3C validator |