Theorem fnopfvb

Description: Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995)

	Ref	Expression
Assertion	fnopfvb	$$⊢\left(FFnA\wedge B\in A\right)\to \left(F\left(B\right)=C\leftrightarrow ⟨B,C⟩\in F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnbrfvb	$$⊢\left(FFnA\wedge B\in A\right)\to \left(F\left(B\right)=C\leftrightarrow BFC\right)$$
2		df-br	$$⊢BFC\leftrightarrow ⟨B,C⟩\in F$$
3	1 2	bitrdi	$$⊢\left(FFnA\wedge B\in A\right)\to \left(F\left(B\right)=C\leftrightarrow ⟨B,C⟩\in F\right)$$