Users' Mathboxes 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 42473
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 42472 . 2 class SalOn
2 vx . . 3 setvar 𝑥
3 cvv 3492 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1527 . . . . . 6 class 𝑠
65cuni 4830 . . . . 5 class 𝑠
72cv 1527 . . . . 5 class 𝑥
86, 7wceq 1528 . . . 4 wff 𝑠 = 𝑥
9 csalg 42470 . . . 4 class SAlg
108, 4, 9crab 3139 . . 3 class {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥}
112, 3, 10cmpt 5137 . 2 class (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
121, 11wceq 1528 1 wff SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator