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 ⊢FFnA∧B∈A→F''''B=C↔BFC

Proof

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