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 e. dom F /\ ( F ` A ) = B ) ) )

Proof

Step	Hyp	Ref	Expression
1		funrel	|- ( Fun F -> Rel F )
2		releldm	|- ( ( Rel F /\ A F B ) -> A e. dom F )
3	2	ex	|- ( Rel F -> ( A F B -> A e. dom F ) )
4	1 3	syl	|- ( Fun F -> ( A F B -> A e. dom F ) )
5	4	pm4.71rd	|- ( Fun F -> ( A F B <-> ( A e. dom F /\ A F B ) ) )
6		funbrfvb	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> A F B ) )
7	6	pm5.32da	|- ( Fun F -> ( ( A e. dom F /\ ( F ` A ) = B ) <-> ( A e. dom F /\ A F B ) ) )
8	5 7	bitr4d	|- ( Fun F -> ( A F B <-> ( A e. dom F /\ ( F ` A ) = B ) ) )