Theorem rnmptsn

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

	Ref	Expression
Assertion	rnmptsn	$$⊢\mathrm{ran}\left(x\in A⟼\left\{x\right\}\right)=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rnopab	$$⊢\mathrm{ran}\left\{⟨x,u⟩|\left(x\in A\wedge u=\left\{x\right\}\right)\right\}=\left\{u|\exists x\left(x\in A\wedge u=\left\{x\right\}\right)\right\}$$
2		df-mpt	$$⊢\left(x\in A⟼\left\{x\right\}\right)=\left\{⟨x,u⟩|\left(x\in A\wedge u=\left\{x\right\}\right)\right\}$$
3	2	rneqi	$$⊢\mathrm{ran}\left(x\in A⟼\left\{x\right\}\right)=\mathrm{ran}\left\{⟨x,u⟩|\left(x\in A\wedge u=\left\{x\right\}\right)\right\}$$
4		df-rex	$$⊢\exists x\in Au=\left\{x\right\}\leftrightarrow \exists x\left(x\in A\wedge u=\left\{x\right\}\right)$$
5	4	abbii	$$⊢\left\{u|\exists x\in Au=\left\{x\right\}\right\}=\left\{u|\exists x\left(x\in A\wedge u=\left\{x\right\}\right)\right\}$$
6	1 3 5	3eqtr4i	$$⊢\mathrm{ran}\left(x\in A⟼\left\{x\right\}\right)=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$