Theorem elmapdd

Description: Deduction associated with elmapd . (Contributed by SN, 29-Jul-2024)

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

Proof

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