Theorem rnmptsn

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

	Ref	Expression
Assertion	rnmptsn	⊢ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }

Proof

Step	Hyp	Ref	Expression
1		rnopab	⊢ ran { ⟨ 𝑥 , 𝑢 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) } = { 𝑢 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) }
2		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = { ⟨ 𝑥 , 𝑢 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) }
3	2	rneqi	⊢ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = ran { ⟨ 𝑥 , 𝑢 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) }
4		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) )
5	4	abbii	⊢ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } } = { 𝑢 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) }
6	1 3 5	3eqtr4i	⊢ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }