This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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