Metamath Proof Explorer

Theorem funbrafv

Description: The second argument of a binary relation on a function is the function's value, analogous to funbrfv . (Contributed by Alexander van der Vekens, 25-May-2017)

		Ref	Expression
	Assertion	funbrafv	$⊢ Fun F \to (A F B \to (F''' A) = B)$

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2		releldm	$⊢ (Rel F \land A F B) \to A \in dom F$
3		funbrafvb	$⊢ (Fun F \land A \in dom F) \to ((F''' A) = B \leftrightarrow A F B)$
4	3	biimprd	$⊢ (Fun F \land A \in dom F) \to (A F B \to (F''' A) = B)$
5	4	expcom	$⊢ A \in dom F \to (Fun F \to (A F B \to (F''' A) = B))$
6	2 5	syl	$⊢ (Rel F \land A F B) \to (Fun F \to (A F B \to (F''' A) = B))$
7	6	ex	$⊢ Rel F \to (A F B \to (Fun F \to (A F B \to (F''' A) = B)))$
8	7	com14	$⊢ A F B \to (A F B \to (Fun F \to (Rel F \to (F''' A) = B)))$
9	8	pm2.43i	$⊢ A F B \to (Fun F \to (Rel F \to (F''' A) = B))$
10	9	com13	$⊢ Rel F \to (Fun F \to (A F B \to (F''' A) = B))$
11	1 10	syl	$⊢ Fun F \to (Fun F \to (A F B \to (F''' A) = B))$
12	11	pm2.43i	$⊢ Fun F \to (A F B \to (F''' A) = B)$