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 W F '''' A = B A B F

Proof

Step Hyp Ref Expression
1 dfatbrafv2b F defAt A B W F '''' A = B A F B
2 df-br A F B A B F
3 1 2 bitrdi F defAt A B W F '''' A = B A B F