fovcl

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

Step	Hyp	Ref	Expression
1		fovcl.1	$⊢ F : R \times S ⟶ C$
2		ffnov	$⊢ F : R \times S ⟶ C \leftrightarrow (F Fn (R \times S) \land \forall x \in R \forall y \in S x F y \in C)$
3	2	simprbi	$⊢ F : R \times S ⟶ C \to \forall x \in R \forall y \in S x F y \in C$
4	1 3	ax-mp	$⊢ \forall x \in R \forall y \in S x F y \in C$
5		oveq1	$⊢ x = A \to x F y = A F y$
6	5	eleq1d	$⊢ x = A \to (x F y \in C \leftrightarrow A F y \in C)$
7		oveq2	$⊢ y = B \to A F y = A F B$
8	7	eleq1d	$⊢ y = B \to (A F y \in C \leftrightarrow A F B \in C)$
9	6 8	rspc2v	$⊢ (A \in R \land B \in S) \to (\forall x \in R \forall y \in S x F y \in C \to A F B \in C)$
10	4 9	mpi	$⊢ (A \in R \land B \in S) \to A F B \in C$

Metamath Proof Explorer