Theorem sssigagen2

Description: A subset of the generating set is also a subset of the generated sigma-algebra. (Contributed by Thierry Arnoux, 22-Sep-2017)

	Ref	Expression
Assertion	sssigagen2	$$⊢\left(A\in V\wedge B\subseteq A\right)\to B\subseteq 𝛔\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A\in V\wedge B\subseteq A\right)\to B\subseteq A$$
2		sssigagen	$$⊢A\in V\to A\subseteq 𝛔\left(A\right)$$
3	2	adantr	$$⊢\left(A\in V\wedge B\subseteq A\right)\to A\subseteq 𝛔\left(A\right)$$
4	1 3	sstrd	$$⊢\left(A\in V\wedge B\subseteq A\right)\to B\subseteq 𝛔\left(A\right)$$