Definition df-submgm 41780

Description: A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020.)

Assertion

Ref	Expression
df-submgm	|- SubMgm = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )

Distinct variable group:   t, s, x, y

Detailed syntax breakdown of Definition df-submgm

Step	Hyp	Ref	Expression
1		csubmgm 41778	. 2 class SubMgm
2		vs	. . 3 setvar s
3		cmgm 17240	. . 3 class Mgm
4		vx	. . . . . . . . 9 setvar x
5	4	cv 1482	. . . . . . . 8 class x
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1482	. . . . . . . 8 class y
8	2	cv 1482	. . . . . . . . 9 class s
9		cplusg 15941	. . . . . . . . 9 class +g
10	8, 9	cfv 5888	. . . . . . . 8 class ( +g ` s )
11	5, 7, 10	co 6650	. . . . . . 7 class ( x ( +g ` s ) y )
12		vt	. . . . . . . 8 setvar t
13	12	cv 1482	. . . . . . 7 class t
14	11, 13	wcel 1990	. . . . . 6 wff ( x ( +g ` s ) y ) e. t
15	14, 6, 13	wral 2912	. . . . 5 wff A. y e. t ( x ( +g ` s ) y ) e. t
16	15, 4, 13	wral 2912	. . . 4 wff A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t
17		cbs 15857	. . . . . 6 class Base
18	8, 17	cfv 5888	. . . . 5 class ( Base ` s )
19	18	cpw 4158	. . . 4 class ~P ( Base ` s )
20	16, 12, 19	crab 2916	. . 3 class { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t }
21	2, 3, 20	cmpt 4729	. 2 class ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )
22	1, 21	wceq 1483	1 wff SubMgm = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )

This definition is referenced by:  submgmrcl  41782  issubmgm  41789