Definition df-ablo

Description: Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ablo	⊢ AbelOp = { 𝑔 ∈ GrpOp ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cablo	⊢ AbelOp
1		vg	⊢ 𝑔
2		cgr	⊢ GrpOp
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑔
5	4	crn	⊢ ran 𝑔
6		vy	⊢ 𝑦
7	3	cv	⊢ 𝑥
8	6	cv	⊢ 𝑦
9	7 8 4	co	⊢ ( 𝑥 𝑔 𝑦 )
10	8 7 4	co	⊢ ( 𝑦 𝑔 𝑥 )
11	9 10	wceq	⊢ ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 )
12	11 6 5	wral	⊢ ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 )
13	12 3 5	wral	⊢ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 )
14	13 1 2	crab	⊢ { 𝑔 ∈ GrpOp ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) }
15	0 14	wceq	⊢ AbelOp = { 𝑔 ∈ GrpOp ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) }