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	$$⊢\mathrm{Com2}=\left\{⟨g,h⟩|\forall a\in \mathrm{ran}g\forall b\in \mathrm{ran}gahb=bha\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccm2	$$class\mathrm{Com2}$$
1		vg	$$setvarg$$
2		vh	$$setvarh$$
3		va	$$setvara$$
4	1	cv	$$setvarg$$
5	4	crn	$$class\mathrm{ran}g$$
6		vb	$$setvarb$$
7	3	cv	$$setvara$$
8	2	cv	$$setvarh$$
9	6	cv	$$setvarb$$
10	7 9 8	co	$$class\left(ahb\right)$$
11	9 7 8	co	$$class\left(bha\right)$$
12	10 11	wceq	$$wffahb=bha$$
13	12 6 5	wral	$$wff\forall b\in \mathrm{ran}gahb=bha$$
14	13 3 5	wral	$$wff\forall a\in \mathrm{ran}g\forall b\in \mathrm{ran}gahb=bha$$
15	14 1 2	copab	$$class\left\{⟨g,h⟩|\forall a\in \mathrm{ran}g\forall b\in \mathrm{ran}gahb=bha\right\}$$
16	0 15	wceq	$$wff\mathrm{Com2}=\left\{⟨g,h⟩|\forall a\in \mathrm{ran}g\forall b\in \mathrm{ran}gahb=bha\right\}$$