Theorem fovrnda

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

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

Proof

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