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

Metamath Proof Explorer

Theorem frn

Description: The range of a mapping. (Contributed by NM, 3-Aug-1994)

		Ref	Expression
	Assertion	frn	$⊢ F : A ⟶ B \to ran F \subseteq B$

Step	Hyp	Ref	Expression
1		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
2	1	simprbi	$⊢ F : A ⟶ B \to ran F \subseteq B$