Theorem fnopafvb

Description: Equivalence of function value and ordered pair membership, analogous to fnopfvb . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	fnopafvb	$$⊢\left(FFnA\wedge B\in A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}B\right)=C\leftrightarrow ⟨B,C⟩\in F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnbrafvb	$$⊢\left(FFnA\wedge B\in A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}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(\left(F\mathrm{\text{'}\text{'}\text{'}}B\right)=C\leftrightarrow ⟨B,C⟩\in F\right)$$