This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )