According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring ." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by , the field of complex numbers restricted to the integers. In zringring it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir), and zringbas shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring of the ring of integers.
Remark: Instead of using the symbol "ZZrng" analogous to used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra)).