fovcdm

Description: An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006)

		Ref	Expression
	Assertion	fovcdm	$⊢ (F : R \times S ⟶ C \land A \in R \land B \in S) \to A F B \in C$

Step	Hyp	Ref	Expression
1		opelxpi	$⊢ (A \in R \land B \in S) \to ⟨A, B⟩ \in (R \times S)$
2		df-ov	$⊢ A F B = F (⟨A, B⟩)$
3		ffvelcdm	$⊢ (F : R \times S ⟶ C \land ⟨A, B⟩ \in (R \times S)) \to F (⟨A, B⟩) \in C$
4	2 3	eqeltrid	$⊢ (F : R \times S ⟶ C \land ⟨A, B⟩ \in (R \times S)) \to A F B \in C$
5	1 4	sylan2	$⊢ (F : R \times S ⟶ C \land (A \in R \land B \in S)) \to A F B \in C$
6	5	3impb	$⊢ (F : R \times S ⟶ C \land A \in R \land B \in S) \to A F B \in C$

Metamath Proof Explorer