Metamath Proof Explorer

Theorem fveere

Description: The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013)

Ref Expression
Assertion fveere 
|- ( ( A e. ( EE ` N ) /\ I e. ( 1 ... N ) ) -> ( A ` I ) e. RR )

Proof

Step Hyp Ref Expression
1 eleei 
 |-  ( A e. ( EE ` N ) -> A : ( 1 ... N ) --> RR )
2 1 ffvelrnda 
 |-  ( ( A e. ( EE ` N ) /\ I e. ( 1 ... N ) ) -> ( A ` I ) e. RR )