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 = ι x | x F A

Proof

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