Theorem fnbrfvb

Description: Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fnbrfvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝐶 ↔ 𝐵 𝐹 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 )
2		fvex	⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
3		eqeq2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝑥 ↔ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ) )
4		breq2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → ( 𝐵 𝐹 𝑥 ↔ 𝐵 𝐹 ( 𝐹 ‘ 𝐵 ) ) )
5	3 4	bibi12d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → ( ( ( 𝐹 ‘ 𝐵 ) = 𝑥 ↔ 𝐵 𝐹 𝑥 ) ↔ ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐵 𝐹 ( 𝐹 ‘ 𝐵 ) ) ) )
6	5	imbi2d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝑥 ↔ 𝐵 𝐹 𝑥 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐵 𝐹 ( 𝐹 ‘ 𝐵 ) ) ) ) )
7		fneu	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃! 𝑥 𝐵 𝐹 𝑥 )
8		tz6.12c	⊢ ( ∃! 𝑥 𝐵 𝐹 𝑥 → ( ( 𝐹 ‘ 𝐵 ) = 𝑥 ↔ 𝐵 𝐹 𝑥 ) )
9	7 8	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝑥 ↔ 𝐵 𝐹 𝑥 ) )
10	2 6 9	vtocl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐵 𝐹 ( 𝐹 ‘ 𝐵 ) ) )
11	1 10	mpbii	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 𝐹 ( 𝐹 ‘ 𝐵 ) )
12		breq2	⊢ ( ( 𝐹 ‘ 𝐵 ) = 𝐶 → ( 𝐵 𝐹 ( 𝐹 ‘ 𝐵 ) ↔ 𝐵 𝐹 𝐶 ) )
13	11 12	syl5ibcom	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝐶 → 𝐵 𝐹 𝐶 ) )
14		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
15		funbrfv	⊢ ( Fun 𝐹 → ( 𝐵 𝐹 𝐶 → ( 𝐹 ‘ 𝐵 ) = 𝐶 ) )
16	14 15	syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 𝐹 𝐶 → ( 𝐹 ‘ 𝐵 ) = 𝐶 ) )
17	16	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 𝐹 𝐶 → ( 𝐹 ‘ 𝐵 ) = 𝐶 ) )
18	13 17	impbid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝐶 ↔ 𝐵 𝐹 𝐶 ) )