afv2eu

Description: The value of a function at a unique point, analogous to fveu . (Contributed by AV, 5-Sep-2022)

		Ref	Expression
	Assertion	afv2eu	$⊢ \exists! x A F x \to (F'''' A) = ⋃ \{x \| A F x\}$

Step	Hyp	Ref	Expression
1		eubrv	$⊢ \exists! x A F x \to A \in V$
2		euex	$⊢ \exists! x A F x \to \exists x A F x$
3		eldmg	$⊢ A \in V \to (A \in dom F \leftrightarrow \exists x A F x)$
4	2 3	syl5ibrcom	$⊢ \exists! x A F x \to (A \in V \to A \in dom F)$
5	4	impcom	$⊢ (A \in V \land \exists! x A F x) \to A \in dom F$
6		dfdfat2	$⊢ F defAt A \leftrightarrow (A \in dom F \land \exists! x A F x)$
7		dfatafv2iota	$⊢ F defAt A \to (F'''' A) = (ι x \| A F x)$
8		iotauni	$⊢ \exists! x A F x \to (ι x \| A F x) = ⋃ \{x \| A F x\}$
9	7 8	sylan9eq	$⊢ (F defAt A \land \exists! x A F x) \to (F'''' A) = ⋃ \{x \| A F x\}$
10	9	ex	$⊢ F defAt A \to (\exists! x A F x \to (F'''' A) = ⋃ \{x \| A F x\})$
11	6 10	sylbir	$⊢ (A \in dom F \land \exists! x A F x) \to (\exists! x A F x \to (F'''' A) = ⋃ \{x \| A F x\})$
12	11	expcom	$⊢ \exists! x A F x \to (A \in dom F \to (\exists! x A F x \to (F'''' A) = ⋃ \{x \| A F x\}))$
13	12	pm2.43a	$⊢ \exists! x A F x \to (A \in dom F \to (F'''' A) = ⋃ \{x \| A F x\})$
14	13	adantl	$⊢ (A \in V \land \exists! x A F x) \to (A \in dom F \to (F'''' A) = ⋃ \{x \| A F x\})$
15	5 14	mpd	$⊢ (A \in V \land \exists! x A F x) \to (F'''' A) = ⋃ \{x \| A F x\}$
16	1 15	mpancom	$⊢ \exists! x A F x \to (F'''' A) = ⋃ \{x \| A F x\}$

Metamath Proof Explorer