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 1728 through ax-9 1986,
all axioms other than
ax-6 1875 are believed to be theorems of free logic,
although the system
without ax-6 1875 is not complete in free logic.
It is preferred to use ax6ev 1877 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2236 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
Ref | Expression |
---|---|
ax6e | ⊢ ∃𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 2039 | . 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) | |
2 | ax13lem1 2236 | . . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦)) | |
3 | ax6ev 1877 | . . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤 | |
4 | equtr 1935 | . . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦)) | |
5 | 3, 4 | eximii 1754 | . . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦) |
6 | 5 | 19.35i 1795 | . . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
7 | 2, 6 | syl6com 36 | . . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)) |
8 | ax6ev 1877 | . . 3 ⊢ ∃𝑤 𝑤 = 𝑦 | |
9 | 7, 8 | exlimiiv 1846 | . 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
10 | 1, 9 | pm2.61i 175 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1473 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-13 2234 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: ax6 2239 spimt 2241 spim 2242 spimed 2243 spimv 2245 spei 2249 equs4 2278 equsal 2279 equsexALT 2282 equvini 2334 equvel 2335 2ax6elem 2437 axi9 2586 dtrucor2 4828 axextnd 9292 ax8dfeq 30948 bj-axc10 31894 bj-alequex 31895 ax6er 32008 exlimiieq1 32009 wl-exeq 32500 wl-equsald 32504 ax6e2nd 37795 ax6e2ndVD 38166 ax6e2ndALT 38188 spd 42223 |
Copyright terms: Public domain | W3C validator |