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

Proof

Step	Hyp	Ref	Expression
1		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
2		releldm	⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 𝐵 ) → 𝐴 ∈ dom 𝐹 )
3		funbrafvb	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ''' 𝐴 ) = 𝐵 ↔ 𝐴 𝐹 𝐵 ) )
4	3	biimprd	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 𝐹 𝐵 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) )
5	4	expcom	⊢ ( 𝐴 ∈ dom 𝐹 → ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) )
6	2 5	syl	⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) )
7	6	ex	⊢ ( Rel 𝐹 → ( 𝐴 𝐹 𝐵 → ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) ) )
8	7	com14	⊢ ( 𝐴 𝐹 𝐵 → ( 𝐴 𝐹 𝐵 → ( Fun 𝐹 → ( Rel 𝐹 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) ) )
9	8	pm2.43i	⊢ ( 𝐴 𝐹 𝐵 → ( Fun 𝐹 → ( Rel 𝐹 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) )
10	9	com13	⊢ ( Rel 𝐹 → ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) )
11	1 10	syl	⊢ ( Fun 𝐹 → ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) )
12	11	pm2.43i	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ''' 𝐴 ) = 𝐵 ) )