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

Metamath Proof Explorer

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