Theorem dffv3

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

	Ref	Expression
Assertion	dffv3	|- ( F ` A ) = ( iota x x e. ( F " { A } ) )

Proof

Step	Hyp	Ref	Expression
1		df-fv	|- ( F ` A ) = ( iota x A F x )
2		elimasng	|- ( ( A e. _V /\ x e. _V ) -> ( x e. ( F " { A } ) <-> <. A , x >. e. F ) )
3		df-br	|- ( A F x <-> <. A , x >. e. F )
4	2 3	bitr4di	|- ( ( A e. _V /\ x e. _V ) -> ( x e. ( F " { A } ) <-> A F x ) )
5	4	elvd	|- ( A e. _V -> ( x e. ( F " { A } ) <-> A F x ) )
6	5	iotabidv	|- ( A e. _V -> ( iota x x e. ( F " { A } ) ) = ( iota x A F x ) )
7	1 6	eqtr4id	|- ( A e. _V -> ( F ` A ) = ( iota x x e. ( F " { A } ) ) )
8		fvprc	|- ( -. A e. _V -> ( F ` A ) = (/) )
9		snprc	|- ( -. A e. _V <-> { A } = (/) )
10	9	biimpi	|- ( -. A e. _V -> { A } = (/) )
11	10	imaeq2d	|- ( -. A e. _V -> ( F " { A } ) = ( F " (/) ) )
12		ima0	|- ( F " (/) ) = (/)
13	11 12	eqtrdi	|- ( -. A e. _V -> ( F " { A } ) = (/) )
14	13	eleq2d	|- ( -. A e. _V -> ( x e. ( F " { A } ) <-> x e. (/) ) )
15	14	iotabidv	|- ( -. A e. _V -> ( iota x x e. ( F " { A } ) ) = ( iota x x e. (/) ) )
16		noel	|- -. x e. (/)
17	16	nex	|- -. E. x x e. (/)
18		euex	|- ( E! x x e. (/) -> E. x x e. (/) )
19	17 18	mto	|- -. E! x x e. (/)
20		iotanul	|- ( -. E! x x e. (/) -> ( iota x x e. (/) ) = (/) )
21	19 20	ax-mp	|- ( iota x x e. (/) ) = (/)
22	15 21	eqtrdi	|- ( -. A e. _V -> ( iota x x e. ( F " { A } ) ) = (/) )
23	8 22	eqtr4d	|- ( -. A e. _V -> ( F ` A ) = ( iota x x e. ( F " { A } ) ) )
24	7 23	pm2.61i	|- ( F ` A ) = ( iota x x e. ( F " { A } ) )