Metamath Proof Explorer

Theorem elmapfun

Description: A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Stefan O'Rear, 5-May-2015)

		Ref	Expression
	Assertion	elmapfun	$⊢ A \in (B^{C}) \to Fun A$

Step	Hyp	Ref	Expression
1		elmapi	$⊢ A \in (B^{C}) \to A : C ⟶ B$
2	1	ffund	$⊢ A \in (B^{C}) \to Fun A$