Theorem mptsnun

Description: A class B is equal to the union of the class of all singletons of elements of B . (Contributed by ML, 16-Jul-2020)

	Ref	Expression
Hypotheses	mptsnun.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
	mptsnun.r	⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
Assertion	mptsnun	⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 = ∪ ( 𝐹 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mptsnun.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
2		mptsnun.r	⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
3		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
4	3	cbvmptv	⊢ ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = ( 𝑦 ∈ 𝐴 ↦ { 𝑦 } )
5	4	eqcomi	⊢ ( 𝑦 ∈ 𝐴 ↦ { 𝑦 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
6	5 2	mptsnunlem	⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 = ∪ ( ( 𝑦 ∈ 𝐴 ↦ { 𝑦 } ) “ 𝐵 ) )
7	1 4	eqtri	⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ { 𝑦 } )
8	7	imaeq1i	⊢ ( 𝐹 “ 𝐵 ) = ( ( 𝑦 ∈ 𝐴 ↦ { 𝑦 } ) “ 𝐵 )
9	8	unieqi	⊢ ∪ ( 𝐹 “ 𝐵 ) = ∪ ( ( 𝑦 ∈ 𝐴 ↦ { 𝑦 } ) “ 𝐵 )
10	6 9	eqtr4di	⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 = ∪ ( 𝐹 “ 𝐵 ) )