Theorem f1imaen

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 NM, 30-Sep-2004)

	Ref	Expression
Hypothesis	f1imaen.1	|- C e. _V
Assertion	f1imaen	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F " C ) ~~ C )

Proof

Step	Hyp	Ref	Expression
1		f1imaen.1	|- C e. _V
2		f1imaeng	|- ( ( F : A -1-1-> B /\ C C_ A /\ C e. _V ) -> ( F " C ) ~~ C )
3	1 2	mp3an3	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F " C ) ~~ C )