Metamath Proof Explorer

Theorem salincld

Description: The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses salincld.1 φ S SAlg
salincld.2 φ E S
salincld.3 φ F S
Assertion salincld φ E F S


Step Hyp Ref Expression
1 salincld.1 φ S SAlg
2 salincld.2 φ E S
3 salincld.3 φ F S
4 salincl S SAlg E S F S E F S
5 1 2 3 4 syl3anc φ E F S