Metamath Proof Explorer


Theorem fnopafvb

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

Proof

Step Hyp Ref Expression
1 fnbrafvb F Fn A B A F ''' B = C B F C
2 df-br B F C B C F
3 1 2 bitrdi F Fn A B A F ''' B = C B C F