Metamath Proof Explorer

Theorem funopafv2b

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

Ref Expression
Assertion funopafv2b 
|- ( ( 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 fnopafv2b 
 |-  ( ( 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 ) )