dffv3

Description: A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013)

		Ref	Expression
	Assertion	dffv3	$⊢ F (A) = (ι x \| x \in F [\{A\}])$

Step	Hyp	Ref	Expression
1		df-fv	$⊢ F (A) = (ι x \| A F x)$
2		elimasng	$⊢ (A \in V \land x \in V) \to (x \in F [\{A\}] \leftrightarrow ⟨A, x⟩ \in F)$
3		df-br	$⊢ A F x \leftrightarrow ⟨A, x⟩ \in F$
4	2 3	bitr4di	$⊢ (A \in V \land x \in V) \to (x \in F [\{A\}] \leftrightarrow A F x)$
5	4	elvd	$⊢ A \in V \to (x \in F [\{A\}] \leftrightarrow A F x)$
6	5	iotabidv	$⊢ A \in V \to (ι x \| x \in F [\{A\}]) = (ι x \| A F x)$
7	1 6	eqtr4id	$⊢ A \in V \to F (A) = (ι x \| x \in F [\{A\}])$
8		fvprc	$⊢ \neg A \in V \to F (A) = \emptyset$
9		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
10	9	biimpi	$⊢ \neg A \in V \to \{A\} = \emptyset$
11	10	imaeq2d	$⊢ \neg A \in V \to F [\{A\}] = F [\emptyset]$
12		ima0	$⊢ F [\emptyset] = \emptyset$
13	11 12	eqtrdi	$⊢ \neg A \in V \to F [\{A\}] = \emptyset$
14	13	eleq2d	$⊢ \neg A \in V \to (x \in F [\{A\}] \leftrightarrow x \in \emptyset)$
15	14	iotabidv	$⊢ \neg A \in V \to (ι x \| x \in F [\{A\}]) = (ι x \| x \in \emptyset)$
16		noel	$⊢ \neg x \in \emptyset$
17	16	nex	$⊢ \neg \exists x x \in \emptyset$
18		euex	$⊢ \exists! x x \in \emptyset \to \exists x x \in \emptyset$
19	17 18	mto	$⊢ \neg \exists! x x \in \emptyset$
20		iotanul	$⊢ \neg \exists! x x \in \emptyset \to (ι x \| x \in \emptyset) = \emptyset$
21	19 20	ax-mp	$⊢ (ι x \| x \in \emptyset) = \emptyset$
22	15 21	eqtrdi	$⊢ \neg A \in V \to (ι x \| x \in F [\{A\}]) = \emptyset$
23	8 22	eqtr4d	$⊢ \neg A \in V \to F (A) = (ι x \| x \in F [\{A\}])$
24	7 23	pm2.61i	$⊢ F (A) = (ι x \| x \in F [\{A\}])$

Metamath Proof Explorer