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

Metamath Proof Explorer

Theorem funbrfv2b

Description: Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Assertion funbrfv2b ⊢ Fun ⁡ F → A F B ↔ A ∈ dom ⁡ F ∧ F ⁡ A = B

Proof

Step Hyp Ref Expression
1 funrel ⊢ Fun ⁡ F → Rel ⁡ F
2 releldm ⊢ Rel ⁡ F ∧ A F B → A ∈ dom ⁡ F
3 2 ex ⊢ Rel ⁡ F → A F B → A ∈ dom ⁡ F
4 1 3 syl ⊢ Fun ⁡ F → A F B → A ∈ dom ⁡ F
5 4 pm4.71rd ⊢ Fun ⁡ F → A F B ↔ A ∈ dom ⁡ F ∧ A F B
6 funbrfvb ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = B ↔ A F B
7 6 pm5.32da ⊢ Fun ⁡ F → A ∈ dom ⁡ F ∧ F ⁡ A = B ↔ A ∈ dom ⁡ F ∧ A F B
8 5 7 bitr4d ⊢ Fun ⁡ F → A F B ↔ A ∈ dom ⁡ F ∧ F ⁡ A = B