Metamath Proof Explorer
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 𝐵 ) ) |