df-submgm

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)

		Ref	Expression
	Assertion	df-submgm	$⊢ SubMgm = (s \in Mgm ⟼ \{t \in 𝒫 {Base}_{s} \| \forall x \in t \forall y \in t x +_{s} y \in t\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubmgm	$class SubMgm$
1		vs	$setvar s$
2		cmgm	$class Mgm$
3		vt	$setvar t$
4		cbs	$class Base$
5	1	cv	$setvar s$
6	5 4	cfv	$class {Base}_{s}$
7	6	cpw	$class 𝒫 {Base}_{s}$
8		vx	$setvar x$
9	3	cv	$setvar t$
10		vy	$setvar y$
11	8	cv	$setvar x$
12		cplusg	$class +_{𝑔}$
13	5 12	cfv	$class +_{s}$
14	10	cv	$setvar y$
15	11 14 13	co	$class (x +_{s} y)$
16	15 9	wcel	$wff x +_{s} y \in t$
17	16 10 9	wral	$wff \forall y \in t x +_{s} y \in t$
18	17 8 9	wral	$wff \forall x \in t \forall y \in t x +_{s} y \in t$
19	18 3 7	crab	$class \{t \in 𝒫 {Base}_{s} \| \forall x \in t \forall y \in t x +_{s} y \in t\}$
20	1 2 19	cmpt	$class (s \in Mgm ⟼ \{t \in 𝒫 {Base}_{s} \| \forall x \in t \forall y \in t x +_{s} y \in t\})$
21	0 20	wceq	$wff SubMgm = (s \in Mgm ⟼ \{t \in 𝒫 {Base}_{s} \| \forall x \in t \forall y \in t x +_{s} y \in t\})$

Metamath Proof Explorer

Definition df-submgm

Detailed syntax breakdown