![]() |
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 1885 through ax-9 2154,
all axioms other than
ax-6 2057 are believed to be theorems of free logic,
although the system
without ax-6 2057 is not complete in free logic.
It is preferred to use ax6ev 2059 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2410 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
Ref | Expression |
---|---|
ax6e | ⊢ ∃𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 2206 | . 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) | |
2 | ax13lem1 2410 | . . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦)) | |
3 | ax6ev 2059 | . . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤 | |
4 | equtr 2106 | . . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦)) | |
5 | 3, 4 | eximii 1912 | . . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦) |
6 | 5 | 19.35i 1958 | . . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
7 | 2, 6 | syl6com 37 | . . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)) |
8 | ax6ev 2059 | . . 3 ⊢ ∃𝑤 𝑤 = 𝑦 | |
9 | 7, 8 | exlimiiv 2011 | . 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦) |
10 | 1, 9 | pm2.61i 176 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1629 ∃wex 1852 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-12 2203 ax-13 2408 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 |
This theorem is referenced by: ax6 2413 spimt 2415 spim 2416 spimed 2417 spimvALT 2420 spei 2423 equs4 2445 equsal 2446 equsexALT 2448 equvini 2492 equvel 2493 2ax6elem 2597 axi9 2747 dtrucor2 5029 axextnd 9613 ax8dfeq 32033 bj-axc10 33037 bj-alequex 33038 ax6er 33148 exlimiieq1 33149 wl-exeq 33649 wl-equsald 33653 ax6e2nd 39292 ax6e2ndVD 39659 ax6e2ndALT 39681 spd 42946 |
Copyright terms: Public domain | W3C validator |