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	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 \|-

Step	Hyp	Ref	Expression
1		ismgmn0.b	$⊢ B = {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 {Base}_{M}$
4	3	biimpi	$⊢ A \in B \to A \in {Base}_{M}$
5	4	elfvexd	$⊢ A \in B \to M \in 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 \|-

Metamath Proof Explorer