| 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 1809 through ax-9 2118,
all axioms other than
ax-6 1967 are believed to be theorems of free logic,
although the system
without ax-6 1967 is not complete in free logic.
Usage of this theorem is discouraged because it depends on ax-13 2377. It is preferred to use ax6ev 1969 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2379 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax6e | ⊢ ∃𝑥 𝑥 = 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.8a 2181 | . 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) | |
| 2 | ax13lem1 2379 | . . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦)) | |
| 3 | ax6ev 1969 | . . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤 | |
| 4 | equtr 2020 | . . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦)) | |
| 5 | 3, 4 | eximii 1837 | . . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦) |
| 6 | 5 | 19.35i 1878 | . . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
| 7 | 2, 6 | syl6com 37 | . . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)) |
| 8 | ax6ev 1969 | . . 3 ⊢ ∃𝑤 𝑤 = 𝑦 | |
| 9 | 7, 8 | exlimiiv 1931 | . 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
| 10 | 1, 9 | pm2.61i 182 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 ax-13 2377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: ax6 2389 spimt 2391 spim 2392 spimed 2393 spimvALT 2396 spei 2399 equs4 2421 equsal 2422 equsexALT 2424 equvini 2460 equvel 2461 2ax6elem 2475 axi9 2704 dtrucor2 5372 axextnd 10631 ax8dfeq 35799 bj-axc10 36784 bj-alequex 36785 ax6er 36834 exlimiieq1 36835 wl-exeq 37535 wl-equsald 37540 ax6e2nd 44578 ax6e2ndVD 44928 ax6e2ndALT 44950 spd 49197 |
| Copyright terms: Public domain | W3C validator |