Metamath Proof Explorer


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 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 V
3 2 adantr F defAt A B W F '''' A 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 W x = F '''' A F '''' A = x A F x F '''' A = F '''' A A F F '''' A
8 dfdfat2 F defAt A A dom F ∃! x A F x
9 tz6.12c-afv2 ∃! 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 W F '''' A = x A F x
12 3 7 11 vtocld F defAt A B W F '''' A = F '''' A A F F '''' A
13 1 12 mpbii F defAt A B 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 W F '''' A = B A F B
16 df-dfat F defAt A A dom F Fun F A
17 simpll A dom F Fun F A B W A dom F
18 simpr A dom F Fun F A B W B W
19 simpr A dom F Fun F A Fun F A
20 19 adantr A dom F Fun F A B W Fun F A
21 17 18 20 jca31 A dom F Fun F A B W A dom F B W Fun F A
22 16 21 sylanb F defAt A B W A dom F B W Fun F A
23 funressnbrafv2 A dom F B W Fun F A A F B F '''' A = B
24 22 23 syl F defAt A B W A F B F '''' A = B
25 15 24 impbid F defAt A B W F '''' A = B A F B