Theorem f1imaeng

Description: If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (Contributed by Mario Carneiro, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		f1ores	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]$$
2		f1oeng	$$⊢\left(C\in V\wedge \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]\right)\to C\approx F\left[C\right]$$
3	2	ancoms	$$⊢\left(\left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]\wedge C\in V\right)\to C\approx F\left[C\right]$$
4	1 3	stoic3	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\wedge C\in V\right)\to C\approx F\left[C\right]$$
5	4	ensymd	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\wedge C\in V\right)\to F\left[C\right]\approx C$$