Metamath Proof Explorer

Theorem fnopafv2b

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

Ref Expression
Assertion fnopafv2b 
|- ( ( F Fn A /\ B e. A ) -> ( ( F '''' B ) = C <-> <. B , C >. e. F ) )

Proof

Step Hyp Ref Expression
1 fnbrafv2b 
 |-  ( ( 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 ) )