Theorem fnbr

Description: The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004)

	Ref	Expression
Assertion	fnbr	|- ( ( F Fn A /\ B F C ) -> B e. A )

Proof

Step	Hyp	Ref	Expression
1		fnrel	|- ( F Fn A -> Rel F )
2		releldm	|- ( ( Rel F /\ B F C ) -> B e. dom F )
3	1 2	sylan	|- ( ( F Fn A /\ B F C ) -> B e. dom F )
4		fndm	|- ( F Fn A -> dom F = A )
5	4	eleq2d	|- ( F Fn A -> ( B e. dom F <-> B e. A ) )
6	5	biimpa	|- ( ( F Fn A /\ B e. dom F ) -> B e. A )
7	3 6	syldan	|- ( ( F Fn A /\ B F C ) -> B e. A )