Metamath Proof Explorer


Theorem fnopfv

Description: Ordered pair with function value. Part of Theorem 4.3(i) of Monk1 p. 41. (Contributed by NM, 30-Sep-2004)

Ref Expression
Assertion fnopfv ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 funfvop ( ( Fun 𝐹𝐵 ∈ dom 𝐹 ) → ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ ∈ 𝐹 )
2 1 funfni ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ ∈ 𝐹 )