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	⊢ 𝑥 = 𝑥

Proof

Step	Hyp	Ref	Expression
1		ax7v1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝑥 → 𝑥 = 𝑥 ) )
2	1	pm2.43i	⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑥 )
3		ax6ev	⊢ ∃ 𝑦 𝑦 = 𝑥
4	2 3	exlimiiv	⊢ 𝑥 = 𝑥