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 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ 𝐹 )