Theorem funfvop

Description: Ordered pair with function value. Part of Theorem 4.3(i) of Monk1 p. 41. (Contributed by NM, 14-Oct-1996)

	Ref	Expression
Assertion	funfvop	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )
2		funopfvb	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
3	1 2	mpbii	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )