Definition df-sate 33306

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 33300	. 2 class Sat∈
2		vm	. . 3 setvar 𝑚
3		vu	. . 3 setvar 𝑢
4		cvv 3432	. . 3 class V
5	3	cv 1538	. . . 4 class 𝑢
6		com 7712	. . . . 5 class ω
7	2	cv 1538	. . . . . 6 class 𝑚
8		cep 5494	. . . . . . 7 class E
9	7, 7	cxp 5587	. . . . . . 7 class (𝑚 × 𝑚)
10	8, 9	cin 3886	. . . . . 6 class ( E ∩ (𝑚 × 𝑚))
11		csat 33298	. . . . . 6 class Sat
12	7, 10, 11	co 7275	. . . . 5 class (𝑚 Sat ( E ∩ (𝑚 × 𝑚)))
13	6, 12	cfv 6433	. . . 4 class ((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)
14	5, 13	cfv 6433	. . 3 class (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢)
15	2, 3, 4, 4, 14	cmpo 7277	. 2 class (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
16	1, 15	wceq 1539	1 wff Sat∈ = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))

This definition is referenced by:  satefv  33376