Metamath Proof Explorer

Theorem elmapi

Description: A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	elmapi	$⊢ A \in (B^{C}) \to A : C ⟶ B$

Step	Hyp	Ref	Expression
1		elmapex	$⊢ A \in (B^{C}) \to (B \in V \land C \in V)$
2		elmapg	$⊢ (B \in V \land C \in V) \to (A \in (B^{C}) \leftrightarrow A : C ⟶ B)$
3	1 2	syl	$⊢ A \in (B^{C}) \to (A \in (B^{C}) \leftrightarrow A : C ⟶ B)$
4	3	ibi	$⊢ A \in (B^{C}) \to A : C ⟶ B$