Metamath Proof Explorer


Theorem funbrafv

Description: The second argument of a binary relation on a function is the function's value, analogous to funbrfv . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion funbrafv Fun F A F B F ''' A = B

Proof

Step Hyp Ref Expression
1 funrel Fun F Rel F
2 releldm Rel F A F B A dom F
3 funbrafvb Fun F A dom F F ''' A = B A F B
4 3 biimprd Fun F A dom F A F B F ''' A = B
5 4 expcom A dom F Fun F A F B F ''' A = B
6 2 5 syl Rel F A F B Fun F A F B F ''' A = B
7 6 ex Rel F A F B Fun F A F B F ''' A = B
8 7 com14 A F B A F B Fun F Rel F F ''' A = B
9 8 pm2.43i A F B Fun F Rel F F ''' A = B
10 9 com13 Rel F Fun F A F B F ''' A = B
11 1 10 syl Fun F Fun F A F B F ''' A = B
12 11 pm2.43i Fun F A F B F ''' A = B