Result on D467: Injective map
Identity map is injection

Let $X$ be a D11: Set.
Let $I : X \to Y$ be an D440: Identity map on $X$.
Then $I$ is a D467: Injective map.
Proofs

Let $X$ be a D11: Set.
Let $I : X \to Y$ be an D440: Identity map on $X$.
If $x, y \in X$ are such $I$ maps them on to the same value, then $$x = I(x) = I(y) = y$$ which establishes injectivity of $I$. $\square$