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	|- ( ( F Fn A /\ B e. A ) -> ( ( F ''' B ) = C <-> <. B , C >. e. F ) )

Proof

Step	Hyp	Ref	Expression
1		fnbrafvb	|- ( ( F Fn A /\ B e. A ) -> ( ( F ''' B ) = C <-> B F C ) )
2		df-br	|- ( B F C <-> <. B , C >. e. F )
3	1 2	bitrdi	|- ( ( F Fn A /\ B e. A ) -> ( ( F ''' B ) = C <-> <. B , C >. e. F ) )