Theorem f1imaen3g

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

Proof

Step	Hyp	Ref	Expression
1		resexg	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝐶 ) ∈ V )
2	1	3ad2ant3	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ↾ 𝐶 ) ∈ V )
3		f1ores	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
4	3	3adant3	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
5		f1oen3g	⊢ ( ( ( 𝐹 ↾ 𝐶 ) ∈ V ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) )
6	2 4 5	syl2anc	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉 ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) )