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=x\to \left(y=x\to x=x\right)$$
2	1	pm2.43i	$$⊢y=x\to x=x$$
3		ax6ev	$$⊢\exists yy=x$$
4	2 3	exlimiiv	$$⊢x=x$$