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 \land B F C) \to B \in A$

Step	Hyp	Ref	Expression
1		fnrel	$⊢ F Fn A \to Rel F$
2		releldm	$⊢ (Rel F \land B F C) \to B \in dom F$
3	1 2	sylan	$⊢ (F Fn A \land B F C) \to B \in dom F$
4		fndm	$⊢ F Fn A \to dom F = A$
5	4	eleq2d	$⊢ F Fn A \to (B \in dom F \leftrightarrow B \in A)$
6	5	biimpa	$⊢ (F Fn A \land B \in dom F) \to B \in A$
7	3 6	syldan	$⊢ (F Fn A \land B F C) \to B \in A$

Metamath Proof Explorer