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={\mathrm{Base}}_M$$
	ismgmn0.o	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	ismgmn0	Could not format assertion : No typesetting found for |- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ismgmn0.b	$$⊢B={\mathrm{Base}}_M$$
2		ismgmn0.o	Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3	1	eleq2i	$$⊢A\in B\leftrightarrow A\in {\mathrm{Base}}_M$$
4	3	biimpi	$$⊢A\in B\to A\in {\mathrm{Base}}_M$$
5	4	elfvexd	$$⊢A\in B\to M\in \mathrm{V}$$
6	1 2	ismgm	Could not format ( M e. _V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( M e. _V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
7	5 6	syl	Could not format ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-