Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-salon Structured version   Visualization version   GIF version

Definition df-salon 41320
 Description: Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Assertion
Ref Expression
df-salon SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
Distinct variable group:   𝑥,𝑠

Detailed syntax breakdown of Definition df-salon
StepHypRef Expression
1 csalon 41319 . 2 class SalOn
2 vx . . 3 setvar 𝑥
3 cvv 3414 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1655 . . . . . 6 class 𝑠
65cuni 4660 . . . . 5 class 𝑠
72cv 1655 . . . . 5 class 𝑥
86, 7wceq 1656 . . . 4 wff 𝑠 = 𝑥
9 csalg 41317 . . . 4 class SAlg
108, 4, 9crab 3121 . . 3 class {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥}
112, 3, 10cmpt 4954 . 2 class (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
121, 11wceq 1656 1 wff SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator