Metamath Proof Explorer


Theorem rnmptsn

Description: The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020)

Ref Expression
Assertion rnmptsn
|- ran ( x e. A |-> { x } ) = { u | E. x e. A u = { x } }

Proof

Step Hyp Ref Expression
1 rnopab
 |-  ran { <. x , u >. | ( x e. A /\ u = { x } ) } = { u | E. x ( x e. A /\ u = { x } ) }
2 df-mpt
 |-  ( x e. A |-> { x } ) = { <. x , u >. | ( x e. A /\ u = { x } ) }
3 2 rneqi
 |-  ran ( x e. A |-> { x } ) = ran { <. x , u >. | ( x e. A /\ u = { x } ) }
4 df-rex
 |-  ( E. x e. A u = { x } <-> E. x ( x e. A /\ u = { x } ) )
5 4 abbii
 |-  { u | E. x e. A u = { x } } = { u | E. x ( x e. A /\ u = { x } ) }
6 1 3 5 3eqtr4i
 |-  ran ( x e. A |-> { x } ) = { u | E. x e. A u = { x } }