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