Metamath Proof Explorer


Theorem efmndfv

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

Ref Expression
Hypotheses efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
Assertion efmndfv ( ( 𝐹𝐵𝑋𝐴 ) → ( 𝐹𝑋 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 1 2 efmndbasf ( 𝐹𝐵𝐹 : 𝐴𝐴 )
4 3 ffvelrnda ( ( 𝐹𝐵𝑋𝐴 ) → ( 𝐹𝑋 ) ∈ 𝐴 )