Metamath Proof Explorer


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