Description: Identity law for equality. Lemma 2 of KalishMontague p. 85. See also Lemma 6 of Tarski p. 68. (Contributed by NM, 1-Apr-2005) (Revised by NM, 9-Apr-2017) (Proof shortened by Wolf Lammen, 22-Aug-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | equid | |- x = x |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax7v1 | |- ( y = x -> ( y = x -> x = x ) ) |
|
| 2 | 1 | pm2.43i | |- ( y = x -> x = x ) |
| 3 | ax6ev | |- E. y y = x |
|
| 4 | 2 3 | exlimiiv | |- x = x |