Theorem dfatbrafv2b

Description: Equivalence of function value and binary relation, analogous to fnbrfvb or funbrfvb . B e. _V is required, because otherwise A F B <-> (/) e. F can be true, but ( F '''' A ) = B is always false (because of dfatafv2ex ). (Contributed by AV, 6-Sep-2022)

	Ref	Expression
Assertion	dfatbrafv2b	|- ( ( F defAt A /\ B e. W ) -> ( ( F '''' A ) = B <-> A F B ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( F '''' A ) = ( F '''' A )
2		dfatafv2ex	|- ( F defAt A -> ( F '''' A ) e. _V )
3	2	adantr	|- ( ( F defAt A /\ B e. W ) -> ( F '''' A ) e. _V )
4		eqeq2	|- ( x = ( F '''' A ) -> ( ( F '''' A ) = x <-> ( F '''' A ) = ( F '''' A ) ) )
5		breq2	|- ( x = ( F '''' A ) -> ( A F x <-> A F ( F '''' A ) ) )
6	4 5	bibi12d	|- ( x = ( F '''' A ) -> ( ( ( F '''' A ) = x <-> A F x ) <-> ( ( F '''' A ) = ( F '''' A ) <-> A F ( F '''' A ) ) ) )
7	6	adantl	|- ( ( ( F defAt A /\ B e. W ) /\ x = ( F '''' A ) ) -> ( ( ( F '''' A ) = x <-> A F x ) <-> ( ( F '''' A ) = ( F '''' A ) <-> A F ( F '''' A ) ) ) )
8		dfdfat2	|- ( F defAt A <-> ( A e. dom F /\ E! x A F x ) )
9		tz6.12c-afv2	|- ( E! x A F x -> ( ( F '''' A ) = x <-> A F x ) )
10	8 9	simplbiim	|- ( F defAt A -> ( ( F '''' A ) = x <-> A F x ) )
11	10	adantr	|- ( ( F defAt A /\ B e. W ) -> ( ( F '''' A ) = x <-> A F x ) )
12	3 7 11	vtocld	|- ( ( F defAt A /\ B e. W ) -> ( ( F '''' A ) = ( F '''' A ) <-> A F ( F '''' A ) ) )
13	1 12	mpbii	|- ( ( F defAt A /\ B e. W ) -> A F ( F '''' A ) )
14		breq2	|- ( ( F '''' A ) = B -> ( A F ( F '''' A ) <-> A F B ) )
15	13 14	syl5ibcom	|- ( ( F defAt A /\ B e. W ) -> ( ( F '''' A ) = B -> A F B ) )
16		df-dfat	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
17		simpll	|- ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ B e. W ) -> A e. dom F )
18		simpr	|- ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ B e. W ) -> B e. W )
19		simpr	|- ( ( A e. dom F /\ Fun ( F |` { A } ) ) -> Fun ( F |` { A } ) )
20	19	adantr	|- ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ B e. W ) -> Fun ( F |` { A } ) )
21	17 18 20	jca31	|- ( ( ( A e. dom F /\ Fun ( F |` { A } ) ) /\ B e. W ) -> ( ( A e. dom F /\ B e. W ) /\ Fun ( F |` { A } ) ) )
22	16 21	sylanb	|- ( ( F defAt A /\ B e. W ) -> ( ( A e. dom F /\ B e. W ) /\ Fun ( F |` { A } ) ) )
23		funressnbrafv2	|- ( ( ( A e. dom F /\ B e. W ) /\ Fun ( F |` { A } ) ) -> ( A F B -> ( F '''' A ) = B ) )
24	22 23	syl	|- ( ( F defAt A /\ B e. W ) -> ( A F B -> ( F '''' A ) = B ) )
25	15 24	impbid	|- ( ( F defAt A /\ B e. W ) -> ( ( F '''' A ) = B <-> A F B ) )