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 AVBAB𝛔A

Proof

Step Hyp Ref Expression
1 sssigagen AVA𝛔A
2 1 sselda AVBAB𝛔A