Metamath Proof Explorer

Theorem funressnbrafv2

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

		Ref	Expression
	Assertion	funressnbrafv2	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \to (A F B \to (F'''' A) = B)$

Proof

Step	Hyp	Ref	Expression
1		simpllr	$⊢ (((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \land A F B) \to B \in W$
2		eleq1	$⊢ x = B \to (x \in W \leftrightarrow B \in W)$
3	2	anbi2d	$⊢ x = B \to ((A \in V \land x \in W) \leftrightarrow (A \in V \land B \in W))$
4	3	anbi1d	$⊢ x = B \to (((A \in V \land x \in W) \land Fun ({F ↾}_{\{A\}})) \leftrightarrow ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})))$
5		breq2	$⊢ x = B \to (A F x \leftrightarrow A F B)$
6	4 5	anbi12d	$⊢ x = B \to ((((A \in V \land x \in W) \land Fun ({F ↾}_{\{A\}})) \land A F x) \leftrightarrow (((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \land A F B))$
7		eqeq2	$⊢ x = B \to ((F'''' A) = x \leftrightarrow (F'''' A) = B)$
8	6 7	imbi12d	$⊢ x = B \to (((((A \in V \land x \in W) \land Fun ({F ↾}_{\{A\}})) \land A F x) \to (F'''' A) = x) \leftrightarrow ((((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \land A F B) \to (F'''' A) = B))$
9		id	$⊢ A F x \to A F x$
10		funressneu	$⊢ ((A \in V \land x \in W) \land Fun ({F ↾}_{\{A\}}) \land A F x) \to \exists! x A F x$
11	10	3expa	$⊢ (((A \in V \land x \in W) \land Fun ({F ↾}_{\{A\}})) \land A F x) \to \exists! x A F x$
12		tz6.12-1-afv2	$⊢ (A F x \land \exists! x A F x) \to (F'''' A) = x$
13	9 11 12	syl2an2	$⊢ (((A \in V \land x \in W) \land Fun ({F ↾}_{\{A\}})) \land A F x) \to (F'''' A) = x$
14	8 13	vtoclg	$⊢ B \in W \to ((((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \land A F B) \to (F'''' A) = B)$
15	1 14	mpcom	$⊢ (((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \land A F B) \to (F'''' A) = B$
16	15	ex	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \to (A F B \to (F'''' A) = B)$