Theorem ffrnb

Description: Characterization of a function with domain and codomain (essentially using that the range is always included in the codomain). Generalization of ffrn . (Contributed by BJ, 21-Sep-2024)

	Ref	Expression
Assertion	ffrnb	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
2		dffn3	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
3	2	anbi1i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )
4	1 3	bitri	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )