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 1812 through ax-9 2116,
all axioms other than
ax-6 1971 are believed to be theorems of free logic,
although the system
without ax-6 1971 is not complete in free logic.
Usage of this theorem is discouraged because it depends on ax-13 2372. It is preferred to use ax6ev 1973 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2374 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax6e | ⊢ ∃𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 2174 | . 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) | |
2 | ax13lem1 2374 | . . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦)) | |
3 | ax6ev 1973 | . . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤 | |
4 | equtr 2024 | . . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦)) | |
5 | 3, 4 | eximii 1839 | . . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦) |
6 | 5 | 19.35i 1881 | . . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
7 | 2, 6 | syl6com 37 | . . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)) |
8 | ax6ev 1973 | . . 3 ⊢ ∃𝑤 𝑤 = 𝑦 | |
9 | 7, 8 | exlimiiv 1934 | . 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
10 | 1, 9 | pm2.61i 182 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1537 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-12 2171 ax-13 2372 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 |
This theorem is referenced by: ax6 2384 spimt 2386 spim 2387 spimed 2388 spimvALT 2391 spei 2394 equs4 2416 equsal 2417 equsexALT 2419 equvini 2455 equvel 2456 2ax6elem 2470 axi9 2705 dtrucor2 5295 axextnd 10347 ax8dfeq 33774 bj-axc10 34965 bj-alequex 34966 ax6er 35016 exlimiieq1 35017 wl-exeq 35693 wl-equsald 35698 ax6e2nd 42178 ax6e2ndVD 42528 ax6e2ndALT 42550 spd 46384 |
Copyright terms: Public domain | W3C validator |