Home
Metamath Proof Explorer
< Previous
Next >
Related theorems
Unicode version
Syntax Definition
cgi
8031
Description:
Extend class notation with a function mapping a group operation to the group's identity element.
Assertion
Ref
Expression
cgi
Id
See definition
df-gid
8035
for more information.
Colors of variables:
wff
set
class
Copyright terms:
Public domain