fnov

Description: Representation of a function in terms of its values. (Contributed by NM, 7-Feb-2004) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	fnov	$⊢ F Fn (A \times B) \leftrightarrow F = (x \in A, y \in B ⟼ x F y)$

Step	Hyp	Ref	Expression
1		dffn5	$⊢ F Fn (A \times B) \leftrightarrow F = (z \in (A \times B) ⟼ F (z))$
2		fveq2	$⊢ z = ⟨x, y⟩ \to F (z) = F (⟨x, y⟩)$
3		df-ov	$⊢ x F y = F (⟨x, y⟩)$
4	2 3	eqtr4di	$⊢ z = ⟨x, y⟩ \to F (z) = x F y$
5	4	mpompt	$⊢ (z \in (A \times B) ⟼ F (z)) = (x \in A, y \in B ⟼ x F y)$
6	5	eqeq2i	$⊢ F = (z \in (A \times B) ⟼ F (z)) \leftrightarrow F = (x \in A, y \in B ⟼ x F y)$
7	1 6	bitri	$⊢ F Fn (A \times B) \leftrightarrow F = (x \in A, y \in B ⟼ x F y)$

Metamath Proof Explorer