Metamath Proof Explorer


Definition df-sate

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)

Ref Expression
Assertion df-sate Sat = m V , u V m Sat E m × m ω u

Detailed syntax breakdown

Step Hyp Ref Expression
0 csate class Sat
1 vm setvar m
2 cvv class V
3 vu setvar u
4 1 cv setvar m
5 csat class Sat
6 cep class E
7 4 4 cxp class m × m
8 6 7 cin class E m × m
9 4 8 5 co class m Sat E m × m
10 com class ω
11 10 9 cfv class m Sat E m × m ω
12 3 cv setvar u
13 12 11 cfv class m Sat E m × m ω u
14 1 3 2 2 13 cmpo class m V , u V m Sat E m × m ω u
15 0 14 wceq wff Sat = m V , u V m Sat E m × m ω u