Theorem equid

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.)

Conclusion
\( \vdash x' = x' \)
Proof
ax7v1
l1
pm2.43i _
\( \vdash y = x' \rightarrow x' = x' \)
ax6ev
\( \vdash \exists y \, y = x' \)
exlimiiv l1 _