Metamath Proof Explorer

Theorem f1imaen

Description: A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004)

Ref Expression
Hypothesis f1imaen.1 C V
Assertion f1imaen F : A 1-1 B C A F C C


Step Hyp Ref Expression
1 f1imaen.1 C V
2 f1imaeng F : A 1-1 B C A C V F C C
3 1 2 mp3an3 F : A 1-1 B C A F C C