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