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=\left(x\in A⟼\left\{x\right\}\right)$$
	mptsnun.r	$$⊢R=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
Assertion	mptsnun	$$⊢B\subseteq A\to B=\bigcup F\left[B\right]$$

Proof

Step	Hyp	Ref	Expression
1		mptsnun.f	$$⊢F=\left(x\in A⟼\left\{x\right\}\right)$$
2		mptsnun.r	$$⊢R=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
3		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
4	3	cbvmptv	$$⊢\left(x\in A⟼\left\{x\right\}\right)=\left(y\in A⟼\left\{y\right\}\right)$$
5	4	eqcomi	$$⊢\left(y\in A⟼\left\{y\right\}\right)=\left(x\in A⟼\left\{x\right\}\right)$$
6	5 2	mptsnunlem	$$⊢B\subseteq A\to B=\bigcup \left(y\in A⟼\left\{y\right\}\right)\left[B\right]$$
7	1 4	eqtri	$$⊢F=\left(y\in A⟼\left\{y\right\}\right)$$
8	7	imaeq1i	$$⊢F\left[B\right]=\left(y\in A⟼\left\{y\right\}\right)\left[B\right]$$
9	8	unieqi	$$⊢\bigcup F\left[B\right]=\bigcup \left(y\in A⟼\left\{y\right\}\right)\left[B\right]$$
10	6 9	syl6eqr	$$⊢B\subseteq A\to B=\bigcup F\left[B\right]$$