Metamath Proof Explorer

Theorem fnbrafv2b

Description: Equivalence of function value and binary relation, analogous to fnbrfvb . (Contributed by AV, 6-Sep-2022)

Ref Expression
Assertion fnbrafv2b ⊢ F Fn A ∧ B ∈ A → F '''' B = C ↔ B F C

Proof

Step Hyp Ref Expression
1 eqid ⊢ F '''' B = F '''' B
2 fundmdfat ⊢ Fun ⁡ F ∧ B ∈ dom ⁡ F → F defAt B
3 2 funfni ⊢ F Fn A ∧ B ∈ A → F defAt B
4 dfatafv2ex ⊢ F defAt B → F '''' B ∈ V
5 3 4 syl ⊢ F Fn A ∧ B ∈ A → F '''' B ∈ V
6 eqeq2 ⊢ x = F '''' B → F '''' B = x ↔ F '''' B = F '''' B
7 breq2 ⊢ x = F '''' B → B F x ↔ B F F '''' B
8 6 7 bibi12d ⊢ x = F '''' B → F '''' B = x ↔ B F x ↔ F '''' B = F '''' B ↔ B F F '''' B
9 8 adantl ⊢ F Fn A ∧ B ∈ A ∧ x = F '''' B → F '''' B = x ↔ B F x ↔ F '''' B = F '''' B ↔ B F F '''' B
10 fneu ⊢ F Fn A ∧ B ∈ A → ∃! x B F x
11 tz6.12c-afv2 ⊢ ∃! x B F x → F '''' B = x ↔ B F x
12 10 11 syl ⊢ F Fn A ∧ B ∈ A → F '''' B = x ↔ B F x
13 5 9 12 vtocld ⊢ F Fn A ∧ B ∈ A → F '''' B = F '''' B ↔ B F F '''' B
14 1 13 mpbii ⊢ F Fn A ∧ B ∈ A → B F F '''' B
15 breq2 ⊢ F '''' B = C → B F F '''' B ↔ B F C
16 14 15 syl5ibcom ⊢ F Fn A ∧ B ∈ A → F '''' B = C → B F C
17 fnfun ⊢ F Fn A → Fun ⁡ F
18 funbrafv2 ⊢ Fun ⁡ F → B F C → F '''' B = C
19 17 18 syl ⊢ F Fn A → B F C → F '''' B = C
20 19 adantr ⊢ F Fn A ∧ B ∈ A → B F C → F '''' B = C
21 16 20 impbid ⊢ F Fn A ∧ B ∈ A → F '''' B = C ↔ B F C