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 φSSAlg
saldifcld.2 φES
Assertion saldifcld φSES

Proof

Step Hyp Ref Expression
1 saldifcld.1 φSSAlg
2 saldifcld.2 φES
3 saldifcl SSAlgESSES
4 1 2 3 syl2anc φSES