Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prv Unicode version

Definition df-prv 23958
Description: Define the "proves" relation on a set. A wff is true in a model  M if for every valuation  s  e.  ( M  ^m  om ), the interpretation of the wff using the membership relation on  M is true. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-prv  |-  |=  =  { <. m ,  u >.  |  ( m  Sat E  u )  =  ( m  ^m  om ) }
Distinct variable group:    u, m

Detailed syntax breakdown of Definition df-prv
StepHypRef Expression
1 cprv 23937 . 2  class  |=
2 vm . . . . . 6  set  m
32cv 1631 . . . . 5  class  m
4 vu . . . . . 6  set  u
54cv 1631 . . . . 5  class  u
6 csate 23936 . . . . 5  class  Sat E
73, 5, 6co 5874 . . . 4  class  ( m  Sat E  u )
8 com 4672 . . . . 5  class  om
9 cmap 6788 . . . . 5  class  ^m
103, 8, 9co 5874 . . . 4  class  ( m  ^m  om )
117, 10wceq 1632 . . 3  wff  ( m  Sat E  u )  =  ( m  ^m  om )
1211, 2, 4copab 4092 . 2  class  { <. m ,  u >.  |  ( m  Sat E  u
)  =  ( m  ^m  om ) }
131, 12wceq 1632 1  wff  |=  =  { <. m ,  u >.  |  ( m  Sat E  u )  =  ( m  ^m  om ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator