Definition df-com2

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.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccm2	|- Com2
1		vg	|- g
2		vh	|- h
3		va	|- a
4	1	cv	|- g
5	4	crn	|- ran g
6		vb	|- b
7	3	cv	|- a
8	2	cv	|- h
9	6	cv	|- b
10	7 9 8	co	|- ( a h b )
11	9 7 8	co	|- ( b h a )
12	10 11	wceq	|- ( a h b ) = ( b h a )
13	12 6 5	wral	|- A. b e. ran g ( a h b ) = ( b h a )
14	13 3 5	wral	|- A. a e. ran g A. b e. ran g ( a h b ) = ( b h a )
15	14 1 2	copab	|- { <. g , h >. | A. a e. ran g A. b e. ran g ( a h b ) = ( b h a ) }
16	0 15	wceq	|- Com2 = { <. g , h >. | A. a e. ran g A. b e. ran g ( a h b ) = ( b h a ) }