Theorem ismgmALT

Description: The predicate "is a magma". (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	ismgmALT	|- ( M e. V -> ( M e. MgmALT <-> .o. clLaw 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 ) clLaw ( Base ` m ) <-> .o. clLaw B ) )
8		df-mgm2	|- MgmALT = { m | ( +g ` m ) clLaw ( Base ` m ) }
9	7 8	elab2g	|- ( M e. V -> ( M e. MgmALT <-> .o. clLaw B ) )