Definition df-sate 31326

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

Step	Hyp	Ref	Expression
1		csate 31320	. 2 class Sat∈
2		vm	. . 3 setvar 𝑚
3		vu	. . 3 setvar 𝑢
4		cvv 3200	. . 3 class V
5	3	cv 1482	. . . 4 class 𝑢
6		com 7065	. . . . 5 class ω
7	2	cv 1482	. . . . . 6 class 𝑚
8		cep 5028	. . . . . . 7 class E
9	7, 7	cxp 5112	. . . . . . 7 class (𝑚 × 𝑚)
10	8, 9	cin 3573	. . . . . 6 class ( E ∩ (𝑚 × 𝑚))
11		csat 31318	. . . . . 6 class Sat
12	7, 10, 11	co 6650	. . . . 5 class (𝑚 Sat ( E ∩ (𝑚 × 𝑚)))
13	6, 12	cfv 5888	. . . 4 class ((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)
14	5, 13	cfv 5888	. . 3 class (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢)
15	2, 3, 4, 4, 14	cmpt2 6652	. 2 class (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
16	1, 15	wceq 1483	1 wff Sat∈ = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))

This definition is referenced by: (None)