Definition df-com2 33789

Description: A device to add commutativity to various sorts of rings. I use ran g because I suppose g has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)

Assertion

Ref	Expression
df-com2	|- Com2 = { <. g , h >. | A. a e. ran g A. b e. ran g ( a h b ) = ( b h a ) }

Distinct variable group:   g, h, a, b

Detailed syntax breakdown of Definition df-com2

Step	Hyp	Ref	Expression
1		ccm2 33788	. 2 class Com2
2		va	. . . . . . . 8 setvar a
3	2	cv 1482	. . . . . . 7 class a
4		vb	. . . . . . . 8 setvar b
5	4	cv 1482	. . . . . . 7 class b
6		vh	. . . . . . . 8 setvar h
7	6	cv 1482	. . . . . . 7 class h
8	3, 5, 7	co 6650	. . . . . 6 class ( a h b )
9	5, 3, 7	co 6650	. . . . . 6 class ( b h a )
10	8, 9	wceq 1483	. . . . 5 wff ( a h b ) = ( b h a )
11		vg	. . . . . . 7 setvar g
12	11	cv 1482	. . . . . 6 class g
13	12	crn 5115	. . . . 5 class ran g
14	10, 4, 13	wral 2912	. . . 4 wff A. b e. ran g ( a h b ) = ( b h a )
15	14, 2, 13	wral 2912	. . 3 wff A. a e. ran g A. b e. ran g ( a h b ) = ( b h a )
16	15, 11, 6	copab 4712	. 2 class { <. g , h >. | A. a e. ran g A. b e. ran g ( a h b ) = ( b h a ) }
17	1, 16	wceq 1483	1 wff Com2 = { <. g , h >. | A. a e. ran g A. b e. ran g ( a h b ) = ( b h a ) }

This definition is referenced by:  iscom2  33794