Definition df-sate 34366

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 34360	. 2 class Sat∈
2		vm	. . 3 setvar 𝑚
3		vu	. . 3 setvar 𝑢
4		cvv 3475	. . 3 class V
5	3	cv 1541	. . . 4 class 𝑢
6		com 7855	. . . . 5 class ω
7	2	cv 1541	. . . . . 6 class 𝑚
8		cep 5580	. . . . . . 7 class E
9	7, 7	cxp 5675	. . . . . . 7 class (𝑚 × 𝑚)
10	8, 9	cin 3948	. . . . . 6 class ( E ∩ (𝑚 × 𝑚))
11		csat 34358	. . . . . 6 class Sat
12	7, 10, 11	co 7409	. . . . 5 class (𝑚 Sat ( E ∩ (𝑚 × 𝑚)))
13	6, 12	cfv 6544	. . . 4 class ((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)
14	5, 13	cfv 6544	. . 3 class (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢)
15	2, 3, 4, 4, 14	cmpo 7411	. 2 class (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
16	1, 15	wceq 1542	1 wff Sat∈ = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))

This definition is referenced by:  satefv  34436