Metamath Proof Explorer

Theorem elmapfn

Description: A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019)

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

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