Theorem issgrpALT

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

	Ref	Expression
Hypotheses	ismgmALT.b	|- B = ( Base ` M )
	ismgmALT.o	|- .o. = ( +g ` M )
Assertion	issgrpALT	|- ( M e. SGrpALT <-> ( M e. MgmALT /\ .o. assLaw 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	3 2	eqtr4di	|- ( m = M -> ( +g ` m ) = .o. )
5		fveq2	|- ( m = M -> ( Base ` m ) = ( Base ` M ) )
6	5 1	eqtr4di	|- ( m = M -> ( Base ` m ) = B )
7	4 6	breq12d	|- ( m = M -> ( ( +g ` m ) assLaw ( Base ` m ) <-> .o. assLaw B ) )
8		df-sgrp2	|- SGrpALT = { m e. MgmALT | ( +g ` m ) assLaw ( Base ` m ) }
9	7 8	elrab2	|- ( M e. SGrpALT <-> ( M e. MgmALT /\ .o. assLaw B ) )