Theorem 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	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ↔ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffn5	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ↔ 𝐹 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
2		fveq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3		df-ov	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4	2 3	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝑥 𝐹 𝑦 ) )
5	4	mpompt	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) )
6	5	eqeq2i	⊢ ( 𝐹 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) ↔ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) )
7	1 6	bitri	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ↔ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) )