Metamath Proof Explorer
Description: Equivalence of function value and ordered pair membership, analogous to
fnopfvb . (Contributed by Alexander van der Vekens, 25-May-2017)
|
|
Ref |
Expression |
|
Assertion |
fnopafvb |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
fnbrafvb |
|
2 |
|
df-br |
|
3 |
1 2
|
bitrdi |
|