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	|- ( ( F Fn A /\ B e. A ) -> ( ( F ''' B ) = C <-> B F C ) )

Proof

Step	Hyp	Ref	Expression
1		fndm	|- ( F Fn A -> dom F = A )
2		eleq2	|- ( A = dom F -> ( B e. A <-> B e. dom F ) )
3	2	eqcoms	|- ( dom F = A -> ( B e. A <-> B e. dom F ) )
4	3	biimpd	|- ( dom F = A -> ( B e. A -> B e. dom F ) )
5	1 4	syl	|- ( F Fn A -> ( B e. A -> B e. dom F ) )
6	5	imp	|- ( ( F Fn A /\ B e. A ) -> B e. dom F )
7		snssi	|- ( B e. A -> { B } C_ A )
8	7	adantl	|- ( ( F Fn A /\ B e. A ) -> { B } C_ A )
9		fnssresb	|- ( F Fn A -> ( ( F |` { B } ) Fn { B } <-> { B } C_ A ) )
10	9	adantr	|- ( ( F Fn A /\ B e. A ) -> ( ( F |` { B } ) Fn { B } <-> { B } C_ A ) )
11	8 10	mpbird	|- ( ( F Fn A /\ B e. A ) -> ( F |` { B } ) Fn { B } )
12		fnfun	|- ( ( F |` { B } ) Fn { B } -> Fun ( F |` { B } ) )
13	11 12	syl	|- ( ( F Fn A /\ B e. A ) -> Fun ( F |` { B } ) )
14		df-dfat	|- ( F defAt B <-> ( B e. dom F /\ Fun ( F |` { B } ) ) )
15		afvfundmfveq	|- ( F defAt B -> ( F ''' B ) = ( F ` B ) )
16	14 15	sylbir	|- ( ( B e. dom F /\ Fun ( F |` { B } ) ) -> ( F ''' B ) = ( F ` B ) )
17	6 13 16	syl2anc	|- ( ( F Fn A /\ B e. A ) -> ( F ''' B ) = ( F ` B ) )
18	17	eqeq1d	|- ( ( F Fn A /\ B e. A ) -> ( ( F ''' B ) = C <-> ( F ` B ) = C ) )
19		fnbrfvb	|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C <-> B F C ) )
20	18 19	bitrd	|- ( ( F Fn A /\ B e. A ) -> ( ( F ''' B ) = C <-> B F C ) )