Metamath Proof Explorer

Theorem funbrfv

Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2		brrelex2	$⊢ (Rel F \land A F B) \to B \in V$
3	1 2	sylan	$⊢ (Fun F \land A F B) \to B \in V$
4		breq2	$⊢ y = B \to (A F y \leftrightarrow A F B)$
5	4	anbi2d	$⊢ y = B \to ((Fun F \land A F y) \leftrightarrow (Fun F \land A F B))$
6		eqeq2	$⊢ y = B \to (F (A) = y \leftrightarrow F (A) = B)$
7	5 6	imbi12d	$⊢ y = B \to (((Fun F \land A F y) \to F (A) = y) \leftrightarrow ((Fun F \land A F B) \to F (A) = B))$
8		funeu	$⊢ (Fun F \land A F y) \to \exists! y A F y$
9		tz6.12-1	$⊢ (A F y \land \exists! y A F y) \to F (A) = y$
10	8 9	sylan2	$⊢ (A F y \land (Fun F \land A F y)) \to F (A) = y$
11	10	anabss7	$⊢ (Fun F \land A F y) \to F (A) = y$
12	7 11	vtoclg	$⊢ B \in V \to ((Fun F \land A F B) \to F (A) = B)$
13	3 12	mpcom	$⊢ (Fun F \land A F B) \to F (A) = B$
14	13	ex	$⊢ Fun F \to (A F B \to F (A) = B)$