Metamath Proof Explorer


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 A F V C F C

Proof

Step Hyp Ref Expression
1 resexg F V F C V
2 1 3ad2ant3 F : A 1-1 B C A F V F C V
3 f1ores F : A 1-1 B C A F C : C 1-1 onto F C
4 3 3adant3 F : A 1-1 B C A F V F C : C 1-1 onto F C
5 f1oen3g F C V F C : C 1-1 onto F C C F C
6 2 4 5 syl2anc F : A 1-1 B C A F V C F C