Theorem unisn0

Description: The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	unisn0	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing \right\}$$
2		uni0b	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing \leftrightarrow \left\{\varnothing \right\}\subseteq \left\{\varnothing \right\}$$
3	1 2	mpbir	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$