Theorem iscmgmALT

Description: The predicate "is a commutative magma". (Contributed by AV, 20-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	ismgmALT.b	|- B = ( Base ` M )
	ismgmALT.o	|- .o. = ( +g ` M )
Assertion	iscmgmALT	|- ( M e. CMgmALT <-> ( M e. MgmALT /\ .o. comLaw B ) )

Proof

Step	Hyp	Ref	Expression
1		ismgmALT.b	|- B = ( Base ` M )
2		ismgmALT.o	|- .o. = ( +g ` M )
3		fveq2	|- ( m = M -> ( +g ` m ) = ( +g ` M ) )
4		fveq2	|- ( m = M -> ( Base ` m ) = ( Base ` M ) )
5	3 4	breq12d	|- ( m = M -> ( ( +g ` m ) comLaw ( Base ` m ) <-> ( +g ` M ) comLaw ( Base ` M ) ) )
6	2 1	breq12i	|- ( .o. comLaw B <-> ( +g ` M ) comLaw ( Base ` M ) )
7	5 6	bitr4di	|- ( m = M -> ( ( +g ` m ) comLaw ( Base ` m ) <-> .o. comLaw B ) )
8		df-cmgm2	|- CMgmALT = { m e. MgmALT | ( +g ` m ) comLaw ( Base ` m ) }
9	7 8	elrab2	|- ( M e. CMgmALT <-> ( M e. MgmALT /\ .o. comLaw B ) )