Definition df-prv 31342

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 SatE u ) = ( m ^m om ) }

Distinct variable group:   u, m

Detailed syntax breakdown of Definition df-prv

Step	Hyp	Ref	Expression
1		cprv 31321	. 2 class |=
2		vm	. . . . . 6 setvar m
3	2	cv 1482	. . . . 5 class m
4		vu	. . . . . 6 setvar u
5	4	cv 1482	. . . . 5 class u
6		csate 31320	. . . . 5 class SatE
7	3, 5, 6	co 6650	. . . 4 class ( m SatE u )
8		com 7065	. . . . 5 class om
9		cmap 7857	. . . . 5 class ^m
10	3, 8, 9	co 6650	. . . 4 class ( m ^m om )
11	7, 10	wceq 1483	. . 3 wff ( m SatE u ) = ( m ^m om )
12	11, 2, 4	copab 4712	. 2 class { <. m , u >. | ( m SatE u ) = ( m ^m om ) }
13	1, 12	wceq 1483	1 wff |= = { <. m , u >. | ( m SatE u ) = ( m ^m om ) }

This definition is referenced by: (None)