Metamath Proof Explorer

Theorem funressneu

Description: There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu . A e. _V is required because otherwise E! y A F y , see brprcneu . (Contributed by AV, 7-Sep-2022)

		Ref	Expression
	Assertion	funressneu	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to \exists! y A F y$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to A \in V$
2		simp1r	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to B \in W$
3		simp3	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to A F B$
4		breldmg	$⊢ (A \in V \land B \in W \land A F B) \to A \in dom F$
5	1 2 3 4	syl3anc	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to A \in dom F$
6		eldmg	$⊢ A \in dom F \to (A \in dom F \leftrightarrow \exists y A F y)$
7	6	ibi	$⊢ A \in dom F \to \exists y A F y$
8	5 7	syl	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to \exists y A F y$
9		simpl	$⊢ (A \in V \land B \in W) \to A \in V$
10	9	anim1i	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}})) \to (A \in V \land Fun ({F ↾}_{\{A\}}))$
11	10	3adant3	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to (A \in V \land Fun ({F ↾}_{\{A\}}))$
12		funressnmo	$⊢ (A \in V \land Fun ({F ↾}_{\{A\}})) \to \exists^{*} y A F y$
13	11 12	syl	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to \exists^{*} y A F y$
14		moeu	$⊢ \exists^{*} y A F y \leftrightarrow (\exists y A F y \to \exists! y A F y)$
15	13 14	sylib	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to (\exists y A F y \to \exists! y A F y)$
16	8 15	mpd	$⊢ ((A \in V \land B \in W) \land Fun ({F ↾}_{\{A\}}) \land A F B) \to \exists! y A F y$