This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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