ffnov

Description: An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004)

		Ref	Expression
	Assertion	ffnov	$⊢ F : A \times B ⟶ C \leftrightarrow (F Fn (A \times B) \land \forall x \in A \forall y \in B x F y \in C)$

Step	Hyp	Ref	Expression
1		ffnfv	$⊢ F : A \times B ⟶ C \leftrightarrow (F Fn (A \times B) \land \forall w \in (A \times B) F (w) \in C)$
2		fveq2	$⊢ w = ⟨x, y⟩ \to F (w) = F (⟨x, y⟩)$
3		df-ov	$⊢ x F y = F (⟨x, y⟩)$
4	2 3	eqtr4di	$⊢ w = ⟨x, y⟩ \to F (w) = x F y$
5	4	eleq1d	$⊢ w = ⟨x, y⟩ \to (F (w) \in C \leftrightarrow x F y \in C)$
6	5	ralxp	$⊢ \forall w \in (A \times B) F (w) \in C \leftrightarrow \forall x \in A \forall y \in B x F y \in C$
7	6	anbi2i	$⊢ (F Fn (A \times B) \land \forall w \in (A \times B) F (w) \in C) \leftrightarrow (F Fn (A \times B) \land \forall x \in A \forall y \in B x F y \in C)$
8	1 7	bitri	$⊢ F : A \times B ⟶ C \leftrightarrow (F Fn (A \times B) \land \forall x \in A \forall y \in B x F y \in C)$

Metamath Proof Explorer