Metamath Proof Explorer

Theorem fnbrafvb

Description: Equivalence of function value and binary relation, analogous to fnbrfvb . (Contributed by Alexander van der Vekens, 25-May-2017)

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

Proof

Step Hyp Ref Expression
1 fndm ⊢ F Fn A → dom ⁡ F = A
2 eleq2 ⊢ A = dom ⁡ F → B ∈ A ↔ B ∈ dom ⁡ F
3 2 eqcoms ⊢ dom ⁡ F = A → B ∈ A ↔ B ∈ dom ⁡ F
4 3 biimpd ⊢ dom ⁡ F = A → B ∈ A → B ∈ dom ⁡ F
5 1 4 syl ⊢ F Fn A → B ∈ A → B ∈ dom ⁡ F
6 5 imp ⊢ F Fn A ∧ B ∈ A → B ∈ dom ⁡ F
7 snssi ⊢ B ∈ A → B ⊆ A
8 7 adantl ⊢ F Fn A ∧ B ∈ A → B ⊆ A
9 fnssresb ⊢ F Fn A → F ↾ B Fn B ↔ B ⊆ A
10 9 adantr ⊢ F Fn A ∧ B ∈ A → F ↾ B Fn B ↔ B ⊆ A
11 8 10 mpbird ⊢ F Fn A ∧ B ∈ A → F ↾ B Fn B
12 fnfun ⊢ F ↾ B Fn B → Fun ⁡ F ↾ B
13 11 12 syl ⊢ F Fn A ∧ B ∈ A → Fun ⁡ F ↾ B
14 df-dfat ⊢ F defAt B ↔ B ∈ dom ⁡ F ∧ Fun ⁡ F ↾ B
15 afvfundmfveq ⊢ F defAt B → F ''' B = F ⁡ B
16 14 15 sylbir ⊢ B ∈ dom ⁡ F ∧ Fun ⁡ F ↾ B → F ''' B = F ⁡ B
17 6 13 16 syl2anc ⊢ F Fn A ∧ B ∈ A → F ''' B = F ⁡ B
18 17 eqeq1d ⊢ F Fn A ∧ B ∈ A → F ''' B = C ↔ F ⁡ B = C
19 fnbrfvb ⊢ F Fn A ∧ B ∈ A → F ⁡ B = C ↔ B F C
20 18 19 bitrd ⊢ F Fn A ∧ B ∈ A → F ''' B = C ↔ B F C