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