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

Metamath Proof Explorer

Theorem funfvbrb

Description: Two ways to say that A is in the domain of F . (Contributed by Mario Carneiro, 1-May-2014)

Ref Expression
Assertion funfvbrb ⊢ Fun ⁡ F → A ∈ dom ⁡ F ↔ A F F ⁡ A

Proof

Step Hyp Ref Expression
1 funfvop ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A F ⁡ A ∈ F
2 df-br ⊢ A F F ⁡ A ↔ A F ⁡ A ∈ F
3 1 2 sylibr ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A F F ⁡ A
4 funrel ⊢ Fun ⁡ F → Rel ⁡ F
5 releldm ⊢ Rel ⁡ F ∧ A F F ⁡ A → A ∈ dom ⁡ F
6 4 5 sylan ⊢ Fun ⁡ F ∧ A F F ⁡ A → A ∈ dom ⁡ F
7 3 6 impbida ⊢ Fun ⁡ F → A ∈ dom ⁡ F ↔ A F F ⁡ A