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 𝐹 → ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfvop	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
2		df-br	⊢ ( 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
3	1 2	sylibr	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) )
4		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
5		releldm	⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ dom 𝐹 )
6	4 5	sylan	⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ dom 𝐹 )
7	3 6	impbida	⊢ ( Fun 𝐹 → ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )