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	|- F = ( x e. A |-> { x } )
	mptsnun.r	|- R = { u | E. x e. A u = { x } }
Assertion	mptsnun	|- ( B C_ A -> B = U. ( F " B ) )

Proof

Step	Hyp	Ref	Expression
1		mptsnun.f	|- F = ( x e. A |-> { x } )
2		mptsnun.r	|- R = { u | E. x e. A u = { x } }
3		sneq	|- ( x = y -> { x } = { y } )
4	3	cbvmptv	|- ( x e. A |-> { x } ) = ( y e. A |-> { y } )
5	4	eqcomi	|- ( y e. A |-> { y } ) = ( x e. A |-> { x } )
6	5 2	mptsnunlem	|- ( B C_ A -> B = U. ( ( y e. A |-> { y } ) " B ) )
7	1 4	eqtri	|- F = ( y e. A |-> { y } )
8	7	imaeq1i	|- ( F " B ) = ( ( y e. A |-> { y } ) " B )
9	8	unieqi	|- U. ( F " B ) = U. ( ( y e. A |-> { y } ) " B )
10	6 9	eqtr4di	|- ( B C_ A -> B = U. ( F " B ) )