Metamath Proof Explorer


Theorem fnbrafvb

Description: Equivalence of function value and binary relation, analogous to fnbrfvb . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion fnbrafvb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶𝐵 𝐹 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fndm ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
2 eleq2 ( 𝐴 = dom 𝐹 → ( 𝐵𝐴𝐵 ∈ dom 𝐹 ) )
3 2 eqcoms ( dom 𝐹 = 𝐴 → ( 𝐵𝐴𝐵 ∈ dom 𝐹 ) )
4 3 biimpd ( dom 𝐹 = 𝐴 → ( 𝐵𝐴𝐵 ∈ dom 𝐹 ) )
5 1 4 syl ( 𝐹 Fn 𝐴 → ( 𝐵𝐴𝐵 ∈ dom 𝐹 ) )
6 5 imp ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → 𝐵 ∈ dom 𝐹 )
7 snssi ( 𝐵𝐴 → { 𝐵 } ⊆ 𝐴 )
8 7 adantl ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → { 𝐵 } ⊆ 𝐴 )
9 fnssresb ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } ↔ { 𝐵 } ⊆ 𝐴 ) )
10 9 adantr ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } ↔ { 𝐵 } ⊆ 𝐴 ) )
11 8 10 mpbird ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } )
12 fnfun ( ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } → Fun ( 𝐹 ↾ { 𝐵 } ) )
13 11 12 syl ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → Fun ( 𝐹 ↾ { 𝐵 } ) )
14 df-dfat ( 𝐹 defAt 𝐵 ↔ ( 𝐵 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐵 } ) ) )
15 afvfundmfveq ( 𝐹 defAt 𝐵 → ( 𝐹 ''' 𝐵 ) = ( 𝐹𝐵 ) )
16 14 15 sylbir ( ( 𝐵 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐵 } ) ) → ( 𝐹 ''' 𝐵 ) = ( 𝐹𝐵 ) )
17 6 13 16 syl2anc ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐹 ''' 𝐵 ) = ( 𝐹𝐵 ) )
18 17 eqeq1d ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶 ↔ ( 𝐹𝐵 ) = 𝐶 ) )
19 fnbrfvb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹𝐵 ) = 𝐶𝐵 𝐹 𝐶 ) )
20 18 19 bitrd ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶𝐵 𝐹 𝐶 ) )