Metamath Proof Explorer
Description: Equivalence of function value and ordered pair membership, analogous to
fnopfvb or funopfvb . (Contributed by AV, 6-Sep-2022)
|
|
Ref |
Expression |
|
Assertion |
dfatopafv2b |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
dfatbrafv2b |
|
2 |
|
df-br |
|
3 |
1 2
|
bitrdi |
|