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	|- ( ph -> S e. SAlg )
	salincld.2	|- ( ph -> E e. S )
	salincld.3	|- ( ph -> F e. S )
Assertion	salincld	|- ( ph -> ( E i^i F ) e. S )

Proof

Step	Hyp	Ref	Expression
1		salincld.1	|- ( ph -> S e. SAlg )
2		salincld.2	|- ( ph -> E e. S )
3		salincld.3	|- ( ph -> F e. S )
4		salincl	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i F ) e. S )
5	1 2 3 4	syl3anc	|- ( ph -> ( E i^i F ) e. S )