Metamath Proof Explorer


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 } ) )