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 39207
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 39206 . 2 class SalOn
2 vx . . 3 setvar 𝑥
3 cvv 3173 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1474 . . . . . 6 class 𝑠
65cuni 4372 . . . . 5 class 𝑠
72cv 1474 . . . . 5 class 𝑥
86, 7wceq 1475 . . . 4 wff 𝑠 = 𝑥
9 csalg 39204 . . . 4 class SAlg
108, 4, 9crab 2900 . . 3 class {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥}
112, 3, 10cmpt 4643 . 2 class (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
121, 11wceq 1475 1 wff SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator