Metamath Proof Explorer
Description: Any element of a set is also an element of the sigmaalgebra that set
generates. (Contributed by Thierry Arnoux, 27Mar2017)


Ref 
Expression 

Assertion 
elsigagen 
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ( sigaGen ‘ 𝐴 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

sssigagen 
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( sigaGen ‘ 𝐴 ) ) 
2 
1

sselda 
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ( sigaGen ‘ 𝐴 ) ) 