Metamath Proof Explorer

Theorem funbrafv2

Description: The second argument of a binary relation on a function is the function's value, analogous to funbrfv . (Contributed by AV, 6-Sep-2022)

		Ref	Expression
	Assertion	funbrafv2	$⊢ 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	$⊢ x = B \to (A F x \leftrightarrow A F B)$
5	4	anbi2d	$⊢ x = B \to ((Fun F \land A F x) \leftrightarrow (Fun F \land A F B))$
6		eqeq2	$⊢ x = B \to ((F'''' A) = x \leftrightarrow (F'''' A) = B)$
7	5 6	imbi12d	$⊢ x = B \to (((Fun F \land A F x) \to (F'''' A) = x) \leftrightarrow ((Fun F \land A F B) \to (F'''' A) = B))$
8		funeu	$⊢ (Fun F \land A F x) \to \exists! x A F x$
9		tz6.12-1-afv2	$⊢ (A F x \land \exists! x A F x) \to (F'''' A) = x$
10	8 9	sylan2	$⊢ (A F x \land (Fun F \land A F x)) \to (F'''' A) = x$
11	10	anabss7	$⊢ (Fun F \land A F x) \to (F'''' A) = x$
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)$