Metamath Proof Explorer


Theorem issmgrpOLD

Description: Obsolete version of issgrp as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis issmgrpOLD.1 X=domdomG
Assertion issmgrpOLD GAGSemiGrpG:X×XXxXyXzXxGyGz=xGyGz

Proof

Step Hyp Ref Expression
1 issmgrpOLD.1 X=domdomG
2 df-sgrOLD SemiGrp=MagmaAss
3 2 eleq2i GSemiGrpGMagmaAss
4 elin GMagmaAssGMagmaGAss
5 1 ismgmOLD GAGMagmaG:X×XX
6 1 isass GAGAssxXyXzXxGyGz=xGyGz
7 5 6 anbi12d GAGMagmaGAssG:X×XXxXyXzXxGyGz=xGyGz
8 4 7 syl5bb GAGMagmaAssG:X×XXxXyXzXxGyGz=xGyGz
9 3 8 syl5bb GAGSemiGrpG:X×XXxXyXzXxGyGz=xGyGz