# Metamath Proof Explorer

## Theorem funbrfv

Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion funbrfv ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹𝐴 ) = 𝐵 ) )

### Proof

Step Hyp Ref Expression
1 funrel ( Fun 𝐹 → Rel 𝐹 )
2 brrelex2 ( ( Rel 𝐹𝐴 𝐹 𝐵 ) → 𝐵 ∈ V )
3 1 2 sylan ( ( Fun 𝐹𝐴 𝐹 𝐵 ) → 𝐵 ∈ V )
4 breq2 ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦𝐴 𝐹 𝐵 ) )
5 4 anbi2d ( 𝑦 = 𝐵 → ( ( Fun 𝐹𝐴 𝐹 𝑦 ) ↔ ( Fun 𝐹𝐴 𝐹 𝐵 ) ) )
6 eqeq2 ( 𝑦 = 𝐵 → ( ( 𝐹𝐴 ) = 𝑦 ↔ ( 𝐹𝐴 ) = 𝐵 ) )
7 5 6 imbi12d ( 𝑦 = 𝐵 → ( ( ( Fun 𝐹𝐴 𝐹 𝑦 ) → ( 𝐹𝐴 ) = 𝑦 ) ↔ ( ( Fun 𝐹𝐴 𝐹 𝐵 ) → ( 𝐹𝐴 ) = 𝐵 ) ) )
8 funeu ( ( Fun 𝐹𝐴 𝐹 𝑦 ) → ∃! 𝑦 𝐴 𝐹 𝑦 )
9 tz6.12-1 ( ( 𝐴 𝐹 𝑦 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) → ( 𝐹𝐴 ) = 𝑦 )
10 8 9 sylan2 ( ( 𝐴 𝐹 𝑦 ∧ ( Fun 𝐹𝐴 𝐹 𝑦 ) ) → ( 𝐹𝐴 ) = 𝑦 )
11 10 anabss7 ( ( Fun 𝐹𝐴 𝐹 𝑦 ) → ( 𝐹𝐴 ) = 𝑦 )
12 7 11 vtoclg ( 𝐵 ∈ V → ( ( Fun 𝐹𝐴 𝐹 𝐵 ) → ( 𝐹𝐴 ) = 𝐵 ) )
13 3 12 mpcom ( ( Fun 𝐹𝐴 𝐹 𝐵 ) → ( 𝐹𝐴 ) = 𝐵 )
14 13 ex ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹𝐴 ) = 𝐵 ) )