Let $X$ be a D11: Set such that

(i) | $I : X \to Y$ is an D440: Identity map on $X$ |

Then $I$ is an D467: Injective map.

Result R2767
on D467: Injective map

Identity map is an injection

Formulation 0

Let $X$ be a D11: Set such that

(i) | $I : X \to Y$ is an D440: Identity map on $X$ |

Then $I$ is an D467: Injective map.

Subresults

▶ | R301: Canonical identity map is an injection |

Proofs

Let $X$ be a D11: Set such that

(i) | $I : X \to Y$ is an D440: Identity map on $X$ |

For all $x, y \in X$, we have $x = I(x) = I(y) = y$. The claim follows. $\square$