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	|- ( ( F : A -1-1-> B /\ C C_ A /\ C e. V ) -> ( F " C ) ~~ C )

Proof

Step	Hyp	Ref	Expression
1		f1ores	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
2		f1oeng	|- ( ( C e. V /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> C ~~ ( F " C ) )
3	2	ancoms	|- ( ( ( F |` C ) : C -1-1-onto-> ( F " C ) /\ C e. V ) -> C ~~ ( F " C ) )
4	1 3	stoic3	|- ( ( F : A -1-1-> B /\ C C_ A /\ C e. V ) -> C ~~ ( F " C ) )
5	4	ensymd	|- ( ( F : A -1-1-> B /\ C C_ A /\ C e. V ) -> ( F " C ) ~~ C )