Theorem funbrfv2b

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

	Ref	Expression
Assertion	funbrfv2b	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
2		releldm	⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 𝐵 ) → 𝐴 ∈ dom 𝐹 )
3	2	ex	⊢ ( Rel 𝐹 → ( 𝐴 𝐹 𝐵 → 𝐴 ∈ dom 𝐹 ) )
4	1 3	syl	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → 𝐴 ∈ dom 𝐹 ) )
5	4	pm4.71rd	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 ↔ ( 𝐴 ∈ dom 𝐹 ∧ 𝐴 𝐹 𝐵 ) ) )
6		funbrfvb	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ 𝐴 𝐹 𝐵 ) )
7	6	pm5.32da	⊢ ( Fun 𝐹 → ( ( 𝐴 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ↔ ( 𝐴 ∈ dom 𝐹 ∧ 𝐴 𝐹 𝐵 ) ) )
8	5 7	bitr4d	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ) )