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 34335
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 34329 . 2 class Sat
2 vm . . 3 setvar 𝑚
3 vu . . 3 setvar 𝑢
4 cvv 3475 . . 3 class V
53cv 1541 . . . 4 class 𝑢
6 com 7855 . . . . 5 class ω
72cv 1541 . . . . . 6 class 𝑚
8 cep 5580 . . . . . . 7 class E
97, 7cxp 5675 . . . . . . 7 class (𝑚 × 𝑚)
108, 9cin 3948 . . . . . 6 class ( E ∩ (𝑚 × 𝑚))
11 csat 34327 . . . . . 6 class Sat
127, 10, 11co 7409 . . . . 5 class (𝑚 Sat ( E ∩ (𝑚 × 𝑚)))
136, 12cfv 6544 . . . 4 class ((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)
145, 13cfv 6544 . . 3 class (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢)
152, 3, 4, 4, 14cmpo 7411 . 2 class (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
161, 15wceq 1542 1 wff Sat = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
Colors of variables: wff setvar class
This definition is referenced by:  satefv  34405
  Copyright terms: Public domain W3C validator