Theorem f1imaeng

Description: A one-to-one function's image under a subset of its domain 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→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )