Theorem isabl2

Description: The predicate "is an Abelian (commutative) group." (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	iscmn.b	|- B = ( Base ` G )
	iscmn.p	|- .+ = ( +g ` G )
Assertion	isabl2	|- ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscmn.b	|- B = ( Base ` G )
2		iscmn.p	|- .+ = ( +g ` G )
3		isabl	|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
4		grpmnd	|- ( G e. Grp -> G e. Mnd )
5	1 2	iscmn	|- ( G e. CMnd <-> ( G e. Mnd /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
6	5	baib	|- ( G e. Mnd -> ( G e. CMnd <-> A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
7	4 6	syl	|- ( G e. Grp -> ( G e. CMnd <-> A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
8	7	pm5.32i	|- ( ( G e. Grp /\ G e. CMnd ) <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
9	3 8	bitri	|- ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )