Theorem funbrafv2b

Description: Function value in terms of a binary relation, analogous to funbrfv2b . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	funbrafv2b	|- ( 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		funbrafvb	|- ( ( 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 ) ) )