Metamath Proof Explorer

Theorem 0mgm

Description: A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypothesis 0mgm.b 
|- ( Base ` M ) = (/)
Assertion 0mgm 
|- ( M e. V -> M e. Mgm )

Proof

Step Hyp Ref Expression
1 0mgm.b 
 |-  ( Base ` M ) = (/)
2 ral0 
 |-  A. x e. (/) A. y e. (/) ( x ( +g ` M ) y ) e. (/)
3 1 eqcomi 
 |-  (/) = ( Base ` M )
4 eqid 
 |-  ( +g ` M ) = ( +g ` M )
5 3 4 ismgm 
 |-  ( M e. V -> ( M e. Mgm <-> A. x e. (/) A. y e. (/) ( x ( +g ` M ) y ) e. (/) ) )
6 2 5 mpbiri 
 |-  ( M e. V -> M e. Mgm )