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