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 FA=ιx|xFA

Proof

Step Hyp Ref Expression
1 df-fv FA=ιx|AFx
2 elimasng AVxVxFAAxF
3 df-br AFxAxF
4 2 3 bitr4di AVxVxFAAFx
5 4 elvd AVxFAAFx
6 5 iotabidv AVιx|xFA=ιx|AFx
7 1 6 eqtr4id AVFA=ιx|xFA
8 fvprc ¬AVFA=
9 snprc ¬AVA=
10 9 biimpi ¬AVA=
11 10 imaeq2d ¬AVFA=F
12 ima0 F=
13 11 12 eqtrdi ¬AVFA=
14 13 eleq2d ¬AVxFAx
15 14 iotabidv ¬AVιx|xFA=ιx|x
16 noel ¬x
17 16 nex ¬xx
18 euex ∃!xxxx
19 17 18 mto ¬∃!xx
20 iotanul ¬∃!xxιx|x=
21 19 20 ax-mp ιx|x=
22 15 21 eqtrdi ¬AVιx|xFA=
23 8 22 eqtr4d ¬AVFA=ιx|xFA
24 7 23 pm2.61i FA=ιx|xFA