Theorem funopafvb

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

	Ref	Expression
Assertion	funopafvb	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ''' A ) = B <-> <. A , B >. e. F ) )

Proof

Step	Hyp	Ref	Expression
1		funfn	|- ( Fun F <-> F Fn dom F )
2		fnopafvb	|- ( ( F Fn dom F /\ A e. dom F ) -> ( ( F ''' A ) = B <-> <. A , B >. e. F ) )
3	1 2	sylanb	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ''' A ) = B <-> <. A , B >. e. F ) )