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 | |- E. x x = y |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.8a | |- ( x = y -> E. x x = y ) |
|
| 2 | ax13lem1 | |- ( -. x = y -> ( w = y -> A. x w = y ) ) |
|
| 3 | ax6ev | |- E. x x = w |
|
| 4 | equtr | |- ( x = w -> ( w = y -> x = y ) ) |
|
| 5 | 3 4 | eximii | |- E. x ( w = y -> x = y ) |
| 6 | 5 | 19.35i | |- ( A. x w = y -> E. x x = y ) |
| 7 | 2 6 | syl6com | |- ( w = y -> ( -. x = y -> E. x x = y ) ) |
| 8 | ax6ev | |- E. w w = y |
|
| 9 | 7 8 | exlimiiv | |- ( -. x = y -> E. x x = y ) |
| 10 | 1 9 | pm2.61i | |- E. x x = y |