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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax7v1 | |
|
2 | 1 | pm2.43i | |
3 | ax6ev | |
|
4 | 2 3 | exlimiiv | |