Theorem saluni

Description: A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	saluni	$$⊢S\in \mathrm{SAlg}\to \bigcup S\in S$$

Proof

Step	Hyp	Ref	Expression
1		dif0	$$⊢\bigcup S\setminus \varnothing =\bigcup S$$
2		0sal	$$⊢S\in \mathrm{SAlg}\to \varnothing \in S$$
3		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge \varnothing \in S\right)\to \bigcup S\setminus \varnothing \in S$$
4	2 3	mpdan	$$⊢S\in \mathrm{SAlg}\to \bigcup S\setminus \varnothing \in S$$
5	1 4	eqeltrrid	$$⊢S\in \mathrm{SAlg}\to \bigcup S\in S$$