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 V B A B 𝛔 A


Step Hyp Ref Expression
1 sssigagen A V A 𝛔 A
2 1 sselda A V B A B 𝛔 A