Metamath Proof Explorer


Theorem equid

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

Proof

Step Hyp Ref Expression
1 ax7v1 y=xy=xx=x
2 1 pm2.43i y=xx=x
3 ax6ev yy=x
4 2 3 exlimiiv x=x