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	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to ⟨A,F\left(A\right)⟩\in F$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢F\left(A\right)=F\left(A\right)$$
2		funopfvb	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left(F\left(A\right)=F\left(A\right)\leftrightarrow ⟨A,F\left(A\right)⟩\in F\right)$$
3	1 2	mpbii	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to ⟨A,F\left(A\right)⟩\in F$$