Metamath Proof Explorer

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 
|- ( ( A e. V /\ B C_ A ) -> B C_ ( sigaGen ` A ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. V /\ B C_ A ) -> B C_ A )
2 sssigagen 
 |-  ( A e. V -> A C_ ( sigaGen ` A ) )
3 2 adantr 
 |-  ( ( A e. V /\ B C_ A ) -> A C_ ( sigaGen ` A ) )
4 1 3 sstrd 
 |-  ( ( A e. V /\ B C_ A ) -> B C_ ( sigaGen ` A ) )