Theorem climfvd

Description: The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypothesis	climfvd.1	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
Assertion	climfvd	⊢ ( 𝜑 → 𝐴 = ( ⇝ ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		climfvd.1	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
2		climfv	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 = ( ⇝ ‘ 𝐹 ) )
3	1 2	syl	⊢ ( 𝜑 → 𝐴 = ( ⇝ ‘ 𝐹 ) )