Metamath Proof Explorer


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 𝐵 ) )