Metamath Proof Explorer

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	$⊢ F : A ⟶ B \leftrightarrow (F : A ⟶ ran F \land ran F \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
2		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
3	2	anbi1i	$⊢ (F Fn A \land ran F \subseteq B) \leftrightarrow (F : A ⟶ ran F \land ran F \subseteq B)$
4	1 3	bitri	$⊢ F : A ⟶ B \leftrightarrow (F : A ⟶ ran F \land ran F \subseteq B)$