# 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 elimasng
` |-  ( ( A e. _V /\ x e. _V ) -> ( x e. ( F " { A } ) <-> <. A , x >. e. F ) )`
2 df-br
` |-  ( A F x <-> <. A , x >. e. F )`
3 1 2 syl6bbr
` |-  ( ( A e. _V /\ x e. _V ) -> ( x e. ( F " { A } ) <-> A F x ) )`
4 3 elvd
` |-  ( A e. _V -> ( x e. ( F " { A } ) <-> A F x ) )`
5 4 iotabidv
` |-  ( A e. _V -> ( iota x x e. ( F " { A } ) ) = ( iota x A F x ) )`
6 df-fv
` |-  ( F ` A ) = ( iota x A F x )`
7 5 6 syl6reqr
` |-  ( 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 syl6eq
` |-  ( -. 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 syl6eq
` |-  ( -. 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 } ) )`