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