Theorem fnopafv2b

Description: Equivalence of function value and ordered pair membership, analogous to fnopfvb . (Contributed by AV, 6-Sep-2022)

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

Proof

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