Metamath Proof Explorer


Theorem salgencld

Description: SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses salgencld.1 φXV
salgencld.2 S=SalGenX
Assertion salgencld φSSAlg

Proof

Step Hyp Ref Expression
1 salgencld.1 φXV
2 salgencld.2 S=SalGenX
3 salgencl XVSalGenXSAlg
4 1 3 syl φSalGenXSAlg
5 2 4 eqeltrid φSSAlg