Metamath Proof Explorer


Theorem imval

Description: The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion imval A A = A i

Proof

Step Hyp Ref Expression
1 fvoveq1 x = A x i = A i
2 df-im = x x i
3 fvex A i V
4 1 2 3 fvmpt A A = A i