Theorem elmapd

Description: Deduction form of elmapg . (Contributed by BJ, 11-Apr-2020)

	Ref	Expression
Hypotheses	elmapd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	elmapd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	elmapd	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elmapd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		elmapd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		elmapg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )