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	⊢ 𝐶 ∈ V
Assertion	f1imaen	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		f1imaen.1	⊢ 𝐶 ∈ V
2		f1imaeng	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ V ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )
3	1 2	mp3an3	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )