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