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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resexg | ||
2 | 1 | 3ad2ant3 | |
3 | f1ores | ||
4 | 3 | 3adant3 | |
5 | f1oen3g | ||
6 | 2 4 5 | syl2anc |