This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Equivalence of function value and binary relation. (Contributed by NM, 26-Mar-2006)
|
|
Ref |
Expression |
|
Assertion |
funbrfvb |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ 𝐴 𝐹 𝐵 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funfn |
⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 ) |
| 2 |
|
fnbrfvb |
⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ 𝐴 𝐹 𝐵 ) ) |
| 3 |
1 2
|
sylanb |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ 𝐴 𝐹 𝐵 ) ) |