Metamath Proof Explorer

Theorem dfatopafv2b

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

Ref Expression
Assertion dfatopafv2b 
|- ( ( F defAt A /\ B e. W ) -> ( ( F '''' A ) = B <-> <. A , B >. e. F ) )

Proof

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