This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Step	Hyp	Ref	Expression
1		ffrnbd.r	$⊢ φ \to ran F \subseteq B$
2		ffrnb	$⊢ F : A ⟶ B \leftrightarrow (F : A ⟶ ran F \land ran F \subseteq B)$
3	1	biantrud	$⊢ φ \to (F : A ⟶ ran F \leftrightarrow (F : A ⟶ ran F \land ran F \subseteq B))$
4	2 3	bitr4id	$⊢ φ \to (F : A ⟶ B \leftrightarrow F : A ⟶ ran F)$