Metamath Proof Explorer


Theorem fovcdmda

Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypothesis fovcdmd.1 ( 𝜑𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
Assertion fovcdmda ( ( 𝜑 ∧ ( 𝐴𝑅𝐵𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 fovcdmd.1 ( 𝜑𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
2 fovcdm ( ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶𝐴𝑅𝐵𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )
3 1 2 syl3an1 ( ( 𝜑𝐴𝑅𝐵𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )
4 3 3expb ( ( 𝜑 ∧ ( 𝐴𝑅𝐵𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )