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 <-> ( F : A --> ran F /\ ran F C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		df-f	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		dffn3	|- ( F Fn A <-> F : A --> ran F )
3	2	anbi1i	|- ( ( F Fn A /\ ran F C_ B ) <-> ( F : A --> ran F /\ ran F C_ B ) )
4	1 3	bitri	|- ( F : A --> B <-> ( F : A --> ran F /\ ran F C_ B ) )