Metamath Proof Explorer


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 SAlg S S

Proof

Step Hyp Ref Expression
1 dif0 S = S
2 0sal S SAlg S
3 saldifcl S SAlg S S S
4 2 3 mpdan S SAlg S S
5 1 4 eqeltrrid S SAlg S S