afveu

Description: The value of a function at a unique point, analogous to fveu . (Contributed by Alexander van der Vekens, 29-Nov-2017)

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

Step	Hyp	Ref	Expression
1		df-br	$⊢ A F x \leftrightarrow ⟨A, x⟩ \in F$
2	1	eubii	$⊢ \exists! x A F x \leftrightarrow \exists! x ⟨A, x⟩ \in F$
3		eu2ndop1stv	$⊢ \exists! x ⟨A, x⟩ \in F \to A \in V$
4	2 3	sylbi	$⊢ \exists! x A F x \to A \in V$
5		euex	$⊢ \exists! x A F x \to \exists x A F x$
6		eldmg	$⊢ A \in V \to (A \in dom F \leftrightarrow \exists x A F x)$
7	5 6	syl5ibrcom	$⊢ \exists! x A F x \to (A \in V \to A \in dom F)$
8	7	impcom	$⊢ (A \in V \land \exists! x A F x) \to A \in dom F$
9		dfdfat2	$⊢ F defAt A \leftrightarrow (A \in dom F \land \exists! x A F x)$
10		afvfundmfveq	$⊢ F defAt A \to (F''' A) = F (A)$
11		fveu	$⊢ \exists! x A F x \to F (A) = ⋃ \{x \| A F x\}$
12	10 11	sylan9eq	$⊢ (F defAt A \land \exists! x A F x) \to (F''' A) = ⋃ \{x \| A F x\}$
13	12	ex	$⊢ F defAt A \to (\exists! x A F x \to (F''' A) = ⋃ \{x \| A F x\})$
14	9 13	sylbir	$⊢ (A \in dom F \land \exists! x A F x) \to (\exists! x A F x \to (F''' A) = ⋃ \{x \| A F x\})$
15	14	expcom	$⊢ \exists! x A F x \to (A \in dom F \to (\exists! x A F x \to (F''' A) = ⋃ \{x \| A F x\}))$
16	15	pm2.43a	$⊢ \exists! x A F x \to (A \in dom F \to (F''' A) = ⋃ \{x \| A F x\})$
17	16	adantl	$⊢ (A \in V \land \exists! x A F x) \to (A \in dom F \to (F''' A) = ⋃ \{x \| A F x\})$
18	8 17	mpd	$⊢ (A \in V \land \exists! x A F x) \to (F''' A) = ⋃ \{x \| A F x\}$
19	4 18	mpancom	$⊢ \exists! x A F x \to (F''' A) = ⋃ \{x \| A F x\}$

Metamath Proof Explorer