Definition df-sate 36317

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 36311	. 2 class Sat∈
2		vm	. . 3 setvar 𝑚
3		vu	. . 3 setvar 𝑢
4		cvv 3454	. . 3 class V
5	3	cv 1569	. . . 4 class 𝑢
6		com 7911	. . . . 5 class ω
7	2	cv 1569	. . . . . 6 class 𝑚
8		cep 5557	. . . . . . 7 class E
9	7, 7	cxp 5656	. . . . . . 7 class (𝑚 × 𝑚)
10	8, 9	cin 4092	. . . . . 6 class ( E ∩ (𝑚 × 𝑚))
11		csat 36309	. . . . . 6 class Sat
12	7, 10, 11	co 7451	. . . . 5 class (𝑚 Sat ( E ∩ (𝑚 × 𝑚)))
13	6, 12	cfv 6566	. . . 4 class ((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)
14	5, 13	cfv 6566	. . 3 class (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢)
15	2, 3, 4, 4, 14	cmpo 7453	. 2 class (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
16	1, 15	wceq 1570	1 wff Sat∈ = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))

This definition is used by:  satefv  36387