Theorem f1imaen

Description: A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004)

	Ref	Expression
Hypothesis	f1imaen.1	$$⊢C\in \mathrm{V}$$
Assertion	f1imaen	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to F\left[C\right]\approx C$$

Proof

Step	Hyp	Ref	Expression
1		f1imaen.1	$$⊢C\in \mathrm{V}$$
2		f1imaeng	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\wedge C\in \mathrm{V}\right)\to F\left[C\right]\approx C$$
3	1 2	mp3an3	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to F\left[C\right]\approx C$$