![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax6e | Structured version Visualization version GIF 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 1910 through ax-9 2175,
all axioms other than
ax-6 2077 are believed to be theorems of free logic,
although the system
without ax-6 2077 is not complete in free logic.
It is preferred to use ax6ev 2079 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2393 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
Ref | Expression |
---|---|
ax6e | ⊢ ∃𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 2225 | . 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) | |
2 | ax13lem1 2393 | . . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦)) | |
3 | ax6ev 2079 | . . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤 | |
4 | equtr 2127 | . . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦)) | |
5 | 3, 4 | eximii 1937 | . . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦) |
6 | 5 | 19.35i 1983 | . . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
7 | 2, 6 | syl6com 37 | . . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)) |
8 | ax6ev 2079 | . . 3 ⊢ ∃𝑤 𝑤 = 𝑦 | |
9 | 7, 8 | exlimiiv 2032 | . 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
10 | 1, 9 | pm2.61i 177 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1656 ∃wex 1880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-12 2222 ax-13 2391 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 |
This theorem is referenced by: ax6 2405 spimt 2407 spimtOLD 2408 spim 2409 spimed 2410 spimvALT 2413 spei 2416 equs4 2438 equsal 2439 equsexALT 2441 equvini 2477 equvel 2478 2ax6elem 2584 axi9 2800 dtrucor2 5073 axextnd 9729 ax8dfeq 32243 bj-axc10 33242 bj-alequex 33243 ax6er 33345 exlimiieq1 33346 wl-exeq 33866 wl-equsald 33870 wl-dv-sb 33875 ax6e2nd 39603 ax6e2ndVD 39963 ax6e2ndALT 39985 spd 43321 |
Copyright terms: Public domain | W3C validator |