Theorem dffv3

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

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

Proof

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