Definition df-cllaw 41822

Description: The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.)

Assertion

Ref	Expression
df-cllaw	|- clLaw = { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }

Distinct variable group:   m, o, x, y

Detailed syntax breakdown of Definition df-cllaw

Step	Hyp	Ref	Expression
1		ccllaw 41819	. 2 class clLaw
2		vx	. . . . . . . 8 setvar x
3	2	cv 1482	. . . . . . 7 class x
4		vy	. . . . . . . 8 setvar y
5	4	cv 1482	. . . . . . 7 class y
6		vo	. . . . . . . 8 setvar o
7	6	cv 1482	. . . . . . 7 class o
8	3, 5, 7	co 6650	. . . . . 6 class ( x o y )
9		vm	. . . . . . 7 setvar m
10	9	cv 1482	. . . . . 6 class m
11	8, 10	wcel 1990	. . . . 5 wff ( x o y ) e. m
12	11, 4, 10	wral 2912	. . . 4 wff A. y e. m ( x o y ) e. m
13	12, 2, 10	wral 2912	. . 3 wff A. x e. m A. y e. m ( x o y ) e. m
14	13, 6, 9	copab 4712	. 2 class { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }
15	1, 14	wceq 1483	1 wff clLaw = { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }

This definition is referenced by:  iscllaw  41825  clcllaw  41827