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 40294
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 40293 . 2 class SalOn
2 vx . . 3 setvar 𝑥
3 cvv 3195 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1480 . . . . . 6 class 𝑠
65cuni 4427 . . . . 5 class 𝑠
72cv 1480 . . . . 5 class 𝑥
86, 7wceq 1481 . . . 4 wff 𝑠 = 𝑥
9 csalg 40291 . . . 4 class SAlg
108, 4, 9crab 2913 . . 3 class {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥}
112, 3, 10cmpt 4720 . 2 class (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
121, 11wceq 1481 1 wff SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ 𝑠 = 𝑥})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator