Definition df-salon 40531

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

Assertion

Ref	Expression
df-salon	|- SalOn = ( x e. _V |-> { s e. SAlg | U. s = x } )

Distinct variable group:   x, s

Detailed syntax breakdown of Definition df-salon

Step	Hyp	Ref	Expression
1		csalon 40530	. 2 class SalOn
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vs	. . . . . . 7 setvar s
5	4	cv 1482	. . . . . 6 class s
6	5	cuni 4436	. . . . 5 class U. s
7	2	cv 1482	. . . . 5 class x
8	6, 7	wceq 1483	. . . 4 wff U. s = x
9		csalg 40528	. . . 4 class SAlg
10	8, 4, 9	crab 2916	. . 3 class { s e. SAlg | U. s = x }
11	2, 3, 10	cmpt 4729	. 2 class ( x e. _V |-> { s e. SAlg | U. s = x } )
12	1, 11	wceq 1483	1 wff SalOn = ( x e. _V |-> { s e. SAlg | U. s = x } )

This definition is referenced by: (None)