Metamath Proof Explorer


Theorem funfv

Description: A simplified expression for the value of a function when we know it is a function. (Contributed by NM, 22-May-1998)

Ref Expression
Assertion funfv Fun F F A = F A

Proof

Step Hyp Ref Expression
1 fvex F A V
2 1 unisn F A = F A
3 eqid dom F = dom F
4 df-fn F Fn dom F Fun F dom F = dom F
5 3 4 mpbiran2 F Fn dom F Fun F
6 fnsnfv F Fn dom F A dom F F A = F A
7 5 6 sylanbr Fun F A dom F F A = F A
8 7 unieqd Fun F A dom F F A = F A
9 2 8 eqtr3id Fun F A dom F F A = F A
10 9 ex Fun F A dom F F A = F A
11 ndmfv ¬ A dom F F A =
12 ndmima ¬ A dom F F A =
13 12 unieqd ¬ A dom F F A =
14 uni0 =
15 13 14 eqtrdi ¬ A dom F F A =
16 11 15 eqtr4d ¬ A dom F F A = F A
17 10 16 pm2.61d1 Fun F F A = F A