Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cntz Structured version   Visualization version   Unicode version

Definition df-cntz 16971
 Description: Define the centralizer of a subset of a magma, which is the set of elements each of which commutes with each element of the given subset. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Assertion
Ref Expression
df-cntz Cntz
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-cntz
StepHypRef Expression
1 ccntz 16969 . 2 Cntz
2 vm . . 3
3 cvv 3045 . . 3
4 vs . . . 4
52cv 1443 . . . . . 6
6 cbs 15121 . . . . . 6
75, 6cfv 5582 . . . . 5
87cpw 3951 . . . 4
9 vx . . . . . . . . 9
109cv 1443 . . . . . . . 8
11 vy . . . . . . . . 9
1211cv 1443 . . . . . . . 8
13 cplusg 15190 . . . . . . . . 9
145, 13cfv 5582 . . . . . . . 8
1510, 12, 14co 6290 . . . . . . 7
1612, 10, 14co 6290 . . . . . . 7
1715, 16wceq 1444 . . . . . 6
184cv 1443 . . . . . 6
1917, 11, 18wral 2737 . . . . 5
2019, 9, 7crab 2741 . . . 4
214, 8, 20cmpt 4461 . . 3
222, 3, 21cmpt 4461 . 2
231, 22wceq 1444 1 Cntz
 Colors of variables: wff setvar class This definition is referenced by:  cntzfval  16974
 Copyright terms: Public domain W3C validator