Theorem funbrafv2

Description: The second argument of a binary relation on a function is the function's value, analogous to funbrfv . (Contributed by AV, 6-Sep-2022)

	Ref	Expression
Assertion	funbrafv2	⊢ ( 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-afv2	⊢ ( ( 𝐴 𝐹 𝑥 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 )
10	8 9	sylan2	⊢ ( ( 𝐴 𝐹 𝑥 ∧ ( Fun 𝐹 ∧ 𝐴 𝐹 𝑥 ) ) → ( 𝐹 '''' 𝐴 ) = 𝑥 )
11	10	anabss7	⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 )
12	7 11	vtoclg	⊢ ( 𝐵 ∈ V → ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
13	3 12	mpcom	⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 )
14	13	ex	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )