Metamath Proof Explorer

Theorem dfafv2

Description: Alternative definition of ( F ''' A ) using ( FA ) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017) (Revised by AV, 25-Aug-2022)

		Ref	Expression
	Assertion	dfafv2	$⊢ (F''' A) = if (F defAt A, F (A), V)$

Proof

Step	Hyp	Ref	Expression
1		df-fv	$⊢ F (A) = (ι x \| A F x)$
2		simprr	$⊢ (⊤ \land (A \in dom F \land \exists! x A F x)) \to \exists! x A F x$
3		reuaiotaiota	$⊢ \exists! x A F x \leftrightarrow (ι x \| A F x) = ι$
4	2 3	sylib	$⊢ (⊤ \land (A \in dom F \land \exists! x A F x)) \to (ι x \| A F x) = ι$
5	1 4	eqtrid	$⊢ (⊤ \land (A \in dom F \land \exists! x A F x)) \to F (A) = ι$
6		eubrdm	$⊢ \exists! x A F x \to A \in dom F$
7	6	ancri	$⊢ \exists! x A F x \to (A \in dom F \land \exists! x A F x)$
8	7	con3i	$⊢ \neg (A \in dom F \land \exists! x A F x) \to \neg \exists! x A F x$
9	8	adantl	$⊢ (⊤ \land \neg (A \in dom F \land \exists! x A F x)) \to \neg \exists! x A F x$
10		aiotavb	$⊢ \neg \exists! x A F x \leftrightarrow ι = V$
11	9 10	sylib	$⊢ (⊤ \land \neg (A \in dom F \land \exists! x A F x)) \to ι = V$
12	11	eqcomd	$⊢ (⊤ \land \neg (A \in dom F \land \exists! x A F x)) \to V = ι$
13	5 12	ifeqda	$⊢ ⊤ \to if ((A \in dom F \land \exists! x A F x), F (A), V) = ι$
14	13	mptru	$⊢ if ((A \in dom F \land \exists! x A F x), F (A), V) = ι$
15		dfdfat2	$⊢ F defAt A \leftrightarrow (A \in dom F \land \exists! x A F x)$
16		ifbi	$⊢ (F defAt A \leftrightarrow (A \in dom F \land \exists! x A F x)) \to if (F defAt A, F (A), V) = if ((A \in dom F \land \exists! x A F x), F (A), V)$
17	15 16	ax-mp	$⊢ if (F defAt A, F (A), V) = if ((A \in dom F \land \exists! x A F x), F (A), V)$
18		df-afv	$⊢ (F''' A) = ι$
19	14 17 18	3eqtr4ri	$⊢ (F''' A) = if (F defAt A, F (A), V)$