Theorem saldifcld

Description: The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	saldifcld.1	$$⊢\phi \to S\in \mathrm{SAlg}$$
	saldifcld.2	$$⊢\phi \to E\in S$$
Assertion	saldifcld	$$⊢\phi \to \bigcup S\setminus E\in S$$

Proof

Step	Hyp	Ref	Expression
1		saldifcld.1	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		saldifcld.2	$$⊢\phi \to E\in S$$
3		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \bigcup S\setminus E\in S$$
4	1 2 3	syl2anc	$$⊢\phi \to \bigcup S\setminus E\in S$$