Equality is Reflexive

Theorem

That is:

$\forall a: a = a$

Proof

This proof depends on Leibniz's law:

$x = y \dashv \vdash \map P x \iff \map P y$

We are trying to prove $a = a$.

Our assertion, then, is:

$a = a \dashv \vdash \map P a \iff \map P a$

From Law of Identity, $\map P a \iff \map P a$ is a tautology.

Thus $a = a$ is also tautologous, and the theorem holds.

$\blacksquare$