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	|- ( ph -> S e. SAlg )
	saldifcld.2	|- ( ph -> E e. S )
Assertion	saldifcld	|- ( ph -> ( U. S \ E ) e. S )

Proof

Step	Hyp	Ref	Expression
1		saldifcld.1	|- ( ph -> S e. SAlg )
2		saldifcld.2	|- ( ph -> E e. S )
3		saldifcl	|- ( ( S e. SAlg /\ E e. S ) -> ( U. S \ E ) e. S )
4	1 2 3	syl2anc	|- ( ph -> ( U. S \ E ) e. S )