Metamath Proof Explorer


Theorem efmndfv

Description: The function value of an endofunction. (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndbas.g
|- G = ( EndoFMnd ` A )
efmndbas.b
|- B = ( Base ` G )
Assertion efmndfv
|- ( ( F e. B /\ X e. A ) -> ( F ` X ) e. A )

Proof

Step Hyp Ref Expression
1 efmndbas.g
 |-  G = ( EndoFMnd ` A )
2 efmndbas.b
 |-  B = ( Base ` G )
3 1 2 efmndbasf
 |-  ( F e. B -> F : A --> A )
4 3 ffvelrnda
 |-  ( ( F e. B /\ X e. A ) -> ( F ` X ) e. A )