This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnbrfvb

Description: Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fnbrfvb ⊢ F Fn A ∧ B ∈ A → F ⁡ B = C ↔ B F C

Proof

Step Hyp Ref Expression
1 eqid ⊢ F ⁡ B = F ⁡ B
2 fvex ⊢ F ⁡ B ∈ V
3 eqeq2 ⊢ x = F ⁡ B → F ⁡ B = x ↔ F ⁡ B = F ⁡ B
4 breq2 ⊢ x = F ⁡ B → B F x ↔ B F F ⁡ B
5 3 4 bibi12d ⊢ x = F ⁡ B → F ⁡ B = x ↔ B F x ↔ F ⁡ B = F ⁡ B ↔ B F F ⁡ B
6 5 imbi2d ⊢ x = F ⁡ B → F Fn A ∧ B ∈ A → F ⁡ B = x ↔ B F x ↔ F Fn A ∧ B ∈ A → F ⁡ B = F ⁡ B ↔ B F F ⁡ B
7 fneu ⊢ F Fn A ∧ B ∈ A → ∃! x B F x
8 tz6.12c ⊢ ∃! x B F x → F ⁡ B = x ↔ B F x
9 7 8 syl ⊢ F Fn A ∧ B ∈ A → F ⁡ B = x ↔ B F x
10 2 6 9 vtocl ⊢ F Fn A ∧ B ∈ A → F ⁡ B = F ⁡ B ↔ B F F ⁡ B
11 1 10 mpbii ⊢ F Fn A ∧ B ∈ A → B F F ⁡ B
12 breq2 ⊢ F ⁡ B = C → B F F ⁡ B ↔ B F C
13 11 12 syl5ibcom ⊢ F Fn A ∧ B ∈ A → F ⁡ B = C → B F C
14 fnfun ⊢ F Fn A → Fun ⁡ F
15 funbrfv ⊢ Fun ⁡ F → B F C → F ⁡ B = C
16 14 15 syl ⊢ F Fn A → B F C → F ⁡ B = C
17 16 adantr ⊢ F Fn A ∧ B ∈ A → B F C → F ⁡ B = C
18 13 17 impbid ⊢ F Fn A ∧ B ∈ A → F ⁡ B = C ↔ B F C