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 1737 through ax-9 1999,
all axioms other than
ax-6 1888 are believed to be theorems of free logic,
although the system
without ax-6 1888 is not complete in free logic.
It is preferred to use ax6ev 1890 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2248 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
Ref | Expression |
---|---|
ax6e |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 2052 | . 2 | |
2 | ax13lem1 2248 | . . . 4 | |
3 | ax6ev 1890 | . . . . . 6 | |
4 | equtr 1948 | . . . . . 6 | |
5 | 3, 4 | eximii 1764 | . . . . 5 |
6 | 5 | 19.35i 1806 | . . . 4 |
7 | 2, 6 | syl6com 37 | . . 3 |
8 | ax6ev 1890 | . . 3 | |
9 | 7, 8 | exlimiiv 1859 | . 2 |
10 | 1, 9 | pm2.61i 176 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wal 1481 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 |
This theorem is referenced by: ax6 2251 spimt 2253 spim 2254 spimed 2255 spimv 2257 spei 2261 equs4 2290 equsal 2291 equsexALT 2293 equvini 2346 equvel 2347 2ax6elem 2449 axi9 2598 dtrucor2 4901 axextnd 9413 ax8dfeq 31704 bj-axc10 32707 bj-alequex 32708 ax6er 32820 exlimiieq1 32821 wl-exeq 33321 wl-equsald 33325 ax6e2nd 38774 ax6e2ndVD 39144 ax6e2ndALT 39166 spd 42425 |
Copyright terms: Public domain | W3C validator |