Metamath Proof Explorer

Theorem elsigagen

Description: Any element of a set is also an element of the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 27-Mar-2017)

Ref Expression
Assertion elsigagen 
|- ( ( A e. V /\ B e. A ) -> B e. ( sigaGen ` A ) )

Proof

Step Hyp Ref Expression
1 sssigagen 
 |-  ( A e. V -> A C_ ( sigaGen ` A ) )
2 1 sselda 
 |-  ( ( A e. V /\ B e. A ) -> B e. ( sigaGen ` A ) )