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 through ax-9 , all axioms other than ax-6 are believed to be theorems of free logic, although the system without ax-6 is not complete in free logic.
Usage of this theorem is discouraged because it depends on ax-13 . It is preferred to use ax6ev when it is sufficient. (Contributed by NM, 14-May-1993) Shortened after ax13lem1 became available. (Revised by Wolf Lammen, 8-Sep-2018) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax6e | ⊢ ∃ 𝑥 𝑥 = 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.8a | ⊢ ( 𝑥 = 𝑦 → ∃ 𝑥 𝑥 = 𝑦 ) | |
| 2 | ax13lem1 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ∀ 𝑥 𝑤 = 𝑦 ) ) | |
| 3 | ax6ev | ⊢ ∃ 𝑥 𝑥 = 𝑤 | |
| 4 | equtr | ⊢ ( 𝑥 = 𝑤 → ( 𝑤 = 𝑦 → 𝑥 = 𝑦 ) ) | |
| 5 | 3 4 | eximii | ⊢ ∃ 𝑥 ( 𝑤 = 𝑦 → 𝑥 = 𝑦 ) |
| 6 | 5 | 19.35i | ⊢ ( ∀ 𝑥 𝑤 = 𝑦 → ∃ 𝑥 𝑥 = 𝑦 ) |
| 7 | 2 6 | syl6com | ⊢ ( 𝑤 = 𝑦 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 𝑥 = 𝑦 ) ) |
| 8 | ax6ev | ⊢ ∃ 𝑤 𝑤 = 𝑦 | |
| 9 | 7 8 | exlimiiv | ⊢ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 𝑥 = 𝑦 ) |
| 10 | 1 9 | pm2.61i | ⊢ ∃ 𝑥 𝑥 = 𝑦 |