Theorem f1imaen3g

Description: If a set function is one-to-one, then a subset of its domain is equinumerous to the image of that subset. (This version of f1imaeng does not need ax-rep nor ax-pow .) (Contributed by BTernaryTau, 13-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		resexg	|- ( F e. V -> ( F |` C ) e. _V )
2	1	3ad2ant3	|- ( ( F : A -1-1-> B /\ C C_ A /\ F e. V ) -> ( F |` C ) e. _V )
3		f1ores	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
4	3	3adant3	|- ( ( F : A -1-1-> B /\ C C_ A /\ F e. V ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
5		f1oen3g	|- ( ( ( F |` C ) e. _V /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> C ~~ ( F " C ) )
6	2 4 5	syl2anc	|- ( ( F : A -1-1-> B /\ C C_ A /\ F e. V ) -> C ~~ ( F " C ) )