Theorem rnsnf

Description: The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rnsnf.1	|- ( ph -> A e. V )
	rnsnf.2	|- ( ph -> F : { A } --> B )
Assertion	rnsnf	|- ( ph -> ran F = { ( F ` A ) } )

Proof

Step	Hyp	Ref	Expression
1		rnsnf.1	|- ( ph -> A e. V )
2		rnsnf.2	|- ( ph -> F : { A } --> B )
3		elsni	|- ( x e. { A } -> x = A )
4	3	fveq2d	|- ( x e. { A } -> ( F ` x ) = ( F ` A ) )
5	4	mpteq2ia	|- ( x e. { A } |-> ( F ` x ) ) = ( x e. { A } |-> ( F ` A ) )
6	2	feqmptd	|- ( ph -> F = ( x e. { A } |-> ( F ` x ) ) )
7		fvexd	|- ( ph -> ( F ` A ) e. _V )
8		fmptsn	|- ( ( A e. V /\ ( F ` A ) e. _V ) -> { <. A , ( F ` A ) >. } = ( x e. { A } |-> ( F ` A ) ) )
9	1 7 8	syl2anc	|- ( ph -> { <. A , ( F ` A ) >. } = ( x e. { A } |-> ( F ` A ) ) )
10	5 6 9	3eqtr4a	|- ( ph -> F = { <. A , ( F ` A ) >. } )
11	10	rneqd	|- ( ph -> ran F = ran { <. A , ( F ` A ) >. } )
12		rnsnopg	|- ( A e. V -> ran { <. A , ( F ` A ) >. } = { ( F ` A ) } )
13	1 12	syl	|- ( ph -> ran { <. A , ( F ` A ) >. } = { ( F ` A ) } )
14	11 13	eqtrd	|- ( ph -> ran F = { ( F ` A ) } )