![]() |
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 1805 through ax-9 2115,
all axioms other than
ax-6 1964 are believed to be theorems of free logic,
although the system
without ax-6 1964 is not complete in free logic.
Usage of this theorem is discouraged because it depends on ax-13 2374. It is preferred to use ax6ev 1966 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2376 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax6e | ⊢ ∃𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 2178 | . 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) | |
2 | ax13lem1 2376 | . . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦)) | |
3 | ax6ev 1966 | . . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤 | |
4 | equtr 2017 | . . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦)) | |
5 | 3, 4 | eximii 1833 | . . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦) |
6 | 5 | 19.35i 1875 | . . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
7 | 2, 6 | syl6com 37 | . . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)) |
8 | ax6ev 1966 | . . 3 ⊢ ∃𝑤 𝑤 = 𝑦 | |
9 | 7, 8 | exlimiiv 1928 | . 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
10 | 1, 9 | pm2.61i 182 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1534 ∃wex 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-12 2174 ax-13 2374 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 |
This theorem is referenced by: ax6 2386 spimt 2388 spim 2389 spimed 2390 spimvALT 2393 spei 2396 equs4 2418 equsal 2419 equsexALT 2421 equvini 2457 equvel 2458 2ax6elem 2472 axi9 2701 dtrucor2 5377 axextnd 10628 ax8dfeq 35779 bj-axc10 36765 bj-alequex 36766 ax6er 36815 exlimiieq1 36816 wl-exeq 37514 wl-equsald 37519 ax6e2nd 44555 ax6e2ndVD 44905 ax6e2ndALT 44927 spd 48908 |
Copyright terms: Public domain | W3C validator |