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	$$⊢\phi \to S\in \mathrm{SAlg}$$
	salincld.2	$$⊢\phi \to E\in S$$
	salincld.3	$$⊢\phi \to F\in S$$
Assertion	salincld	$$⊢\phi \to E\cap F\in S$$

Proof

Step	Hyp	Ref	Expression
1		salincld.1	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		salincld.2	$$⊢\phi \to E\in S$$
3		salincld.3	$$⊢\phi \to F\in S$$
4		salincl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\cap F\in S$$
5	1 2 3 4	syl3anc	$$⊢\phi \to E\cap F\in S$$