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	$$⊢{\mathrm{Base}}_M=\varnothing$$
Assertion	0mgm	$$⊢M\in V\to M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		0mgm.b	$$⊢{\mathrm{Base}}_M=\varnothing$$
2		ral0	$$⊢\forall x\in \varnothing \forall y\in \varnothing x{+}_{M}y\in \varnothing$$
3	1	eqcomi	$$⊢\varnothing ={\mathrm{Base}}_M$$
4		eqid	$$⊢{+}_M={+}_M$$
5	3 4	ismgm	$$⊢M\in V\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in \varnothing \forall y\in \varnothing x{+}_{M}y\in \varnothing \right)$$
6	2 5	mpbiri	$$⊢M\in V\to M\in \mathrm{Mgm}$$