Metamath Proof Explorer


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 ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴𝐶𝑉 ) → ( 𝐹𝐶 ) ≈ 𝐶 )

Proof

Step Hyp Ref Expression
1 f1ores ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) )
2 f1oeng ( ( 𝐶𝑉 ∧ ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) ) → 𝐶 ≈ ( 𝐹𝐶 ) )
3 2 ancoms ( ( ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) ∧ 𝐶𝑉 ) → 𝐶 ≈ ( 𝐹𝐶 ) )
4 1 3 stoic3 ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴𝐶𝑉 ) → 𝐶 ≈ ( 𝐹𝐶 ) )
5 4 ensymd ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴𝐶𝑉 ) → ( 𝐹𝐶 ) ≈ 𝐶 )