Theorem ffrnbd

Description: A function maps to its range iff the range is a subset of its codomain. Generalization of ffrn . (Contributed by AV, 20-Sep-2024)

	Ref	Expression
Hypothesis	ffrnbd.r	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
Assertion	ffrnbd	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ffrnbd.r	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
2		ffrnb	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )
3	1	biantrud	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ran 𝐹 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) ) )
4	2 3	bitr4id	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 ) )