Theorem ismgmn0

Description: The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Hypotheses	ismgmn0.b	|- B = ( Base ` M )
	ismgmn0.o	|- .o. = ( +g ` M )
Assertion	ismgmn0	|- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		ismgmn0.b	|- B = ( Base ` M )
2		ismgmn0.o	|- .o. = ( +g ` M )
3	1	eleq2i	|- ( A e. B <-> A e. ( Base ` M ) )
4	3	biimpi	|- ( A e. B -> A e. ( Base ` M ) )
5	4	elfvexd	|- ( A e. B -> M e. _V )
6	1 2	ismgm	|- ( M e. _V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
7	5 6	syl	|- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )