Description: Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | submgmmgm.h | ||
Assertion | submgmmgm |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | submgmmgm.h | ||
2 | submgmrcl | ||
3 | eqid | ||
4 | 3 1 | issubmgm2 | |
5 | 2 4 | syl | |
6 | 5 | ibi | |
7 | 6 | simprd |