Metamath Proof Explorer


Definition df-salon

Description: Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion df-salon SalOn = x V s SAlg | s = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 csalon class SalOn
1 vx setvar x
2 cvv class V
3 vs setvar s
4 csalg class SAlg
5 3 cv setvar s
6 5 cuni class s
7 1 cv setvar x
8 6 7 wceq wff s = x
9 8 3 4 crab class s SAlg | s = x
10 1 2 9 cmpt class x V s SAlg | s = x
11 0 10 wceq wff SalOn = x V s SAlg | s = x