Definition df-cllaw

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)

	Ref	Expression
Assertion	df-cllaw	$$⊢\mathrm{clLaw}=\left\{⟨o,m⟩|\forall x\in m\forall y\in mxoy\in m\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccllaw	$$class\mathrm{clLaw}$$
1		vo	$$setvaro$$
2		vm	$$setvarm$$
3		vx	$$setvarx$$
4	2	cv	$$setvarm$$
5		vy	$$setvary$$
6	3	cv	$$setvarx$$
7	1	cv	$$setvaro$$
8	5	cv	$$setvary$$
9	6 8 7	co	$$class\left(xoy\right)$$
10	9 4	wcel	$$wffxoy\in m$$
11	10 5 4	wral	$$wff\forall y\in mxoy\in m$$
12	11 3 4	wral	$$wff\forall x\in m\forall y\in mxoy\in m$$
13	12 1 2	copab	$$class\left\{⟨o,m⟩|\forall x\in m\forall y\in mxoy\in m\right\}$$
14	0 13	wceq	$$wff\mathrm{clLaw}=\left\{⟨o,m⟩|\forall x\in m\forall y\in mxoy\in m\right\}$$