This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) )