Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sate Structured version   Visualization version   GIF version

Definition df-sate 32488
Description: A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable 𝑛. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-sate Sat = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
Distinct variable group:   𝑢,𝑚

Detailed syntax breakdown of Definition df-sate
StepHypRef Expression
1 csate 32482 . 2 class Sat
2 vm . . 3 setvar 𝑚
3 vu . . 3 setvar 𝑢
4 cvv 3492 . . 3 class V
53cv 1527 . . . 4 class 𝑢
6 com 7569 . . . . 5 class ω
72cv 1527 . . . . . 6 class 𝑚
8 cep 5457 . . . . . . 7 class E
97, 7cxp 5546 . . . . . . 7 class (𝑚 × 𝑚)
108, 9cin 3932 . . . . . 6 class ( E ∩ (𝑚 × 𝑚))
11 csat 32480 . . . . . 6 class Sat
127, 10, 11co 7145 . . . . 5 class (𝑚 Sat ( E ∩ (𝑚 × 𝑚)))
136, 12cfv 6348 . . . 4 class ((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)
145, 13cfv 6348 . . 3 class (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢)
152, 3, 4, 4, 14cmpo 7147 . 2 class (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
161, 15wceq 1528 1 wff Sat = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
Colors of variables: wff setvar class
This definition is referenced by:  satefv  32558
  Copyright terms: Public domain W3C validator