This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } )