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	$$⊢\left(FFnA\wedge B\in A\right)\to ⟨B,F\left(B\right)⟩\in F$$

Proof

Step	Hyp	Ref	Expression
1		funfvop	$$⊢\left(\mathrm{Fun}F\wedge B\in \mathrm{dom}F\right)\to ⟨B,F\left(B\right)⟩\in F$$
2	1	funfni	$$⊢\left(FFnA\wedge B\in A\right)\to ⟨B,F\left(B\right)⟩\in F$$