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	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐴 : 𝐶 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elmapex	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
2		elmapg	⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ↔ 𝐴 : 𝐶 ⟶ 𝐵 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ↔ 𝐴 : 𝐶 ⟶ 𝐵 ) )
4	3	ibi	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐴 : 𝐶 ⟶ 𝐵 )