Definition df-sate 31326

Description: A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable n. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-sate	|- SatE = ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` om ) ` u ) )

Distinct variable group:   u, m

Detailed syntax breakdown of Definition df-sate

Step	Hyp	Ref	Expression
1		csate 31320	. 2 class SatE
2		vm	. . 3 setvar m
3		vu	. . 3 setvar u
4		cvv 3200	. . 3 class _V
5	3	cv 1482	. . . 4 class u
6		com 7065	. . . . 5 class om
7	2	cv 1482	. . . . . 6 class m
8		cep 5028	. . . . . . 7 class _E
9	7, 7	cxp 5112	. . . . . . 7 class ( m X. m )
10	8, 9	cin 3573	. . . . . 6 class ( _E i^i ( m X. m ) )
11		csat 31318	. . . . . 6 class Sat
12	7, 10, 11	co 6650	. . . . 5 class ( m Sat ( _E i^i ( m X. m ) ) )
13	6, 12	cfv 5888	. . . 4 class ( ( m Sat ( _E i^i ( m X. m ) ) ) ` om )
14	5, 13	cfv 5888	. . 3 class ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` om ) ` u )
15	2, 3, 4, 4, 14	cmpt2 6652	. 2 class ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` om ) ` u ) )
16	1, 15	wceq 1483	1 wff SatE = ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` om ) ` u ) )

This definition is referenced by: (None)