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 e. SAlg -> U. S e. S )

Proof

Step Hyp Ref Expression
1 dif0 
 |-  ( U. S \ (/) ) = U. S
2 0sal 
 |-  ( S e. SAlg -> (/) e. S )
3 saldifcl 
 |-  ( ( S e. SAlg /\ (/) e. S ) -> ( U. S \ (/) ) e. S )
4 2 3 mpdan 
 |-  ( S e. SAlg -> ( U. S \ (/) ) e. S )
5 1 4 eqeltrrid 
 |-  ( S e. SAlg -> U. S e. S )