Theorem ffrnbd

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

	Ref	Expression
Hypothesis	ffrnbd.r	|- ( ph -> ran F C_ B )
Assertion	ffrnbd	|- ( ph -> ( F : A --> B <-> F : A --> ran F ) )

Proof

Step	Hyp	Ref	Expression
1		ffrnbd.r	|- ( ph -> ran F C_ B )
2		ffrnb	|- ( F : A --> B <-> ( F : A --> ran F /\ ran F C_ B ) )
3	1	biantrud	|- ( ph -> ( F : A --> ran F <-> ( F : A --> ran F /\ ran F C_ B ) ) )
4	2 3	bitr4id	|- ( ph -> ( F : A --> B <-> F : A --> ran F ) )