Result on D467: Injective map
Canonical identity map is injection

Let $X$ be a D11: Set.
Let $I : X \to X$ be a D4428: Canonical identity map on $X$.
Then $I$ is a D467: Injective map.
Proofs

Let $X$ be a D11: Set.
Let $I : X \to X$ be a D4428: Canonical identity map on $X$.
This result is a corollary to R2767: Identity map is injection. $\square$