Metamath Proof Explorer


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 φ S SAlg
saldifcld.2 φ E S
Assertion saldifcld φ S E S

Proof

Step Hyp Ref Expression
1 saldifcld.1 φ S SAlg
2 saldifcld.2 φ E S
3 saldifcl S SAlg E S S E S
4 1 2 3 syl2anc φ S E S