Metamath Proof Explorer

Definition df-zring

Description: The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019)

Ref Expression
Assertion df-zring 
|- ZZring = ( CCfld |`s ZZ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 zring 
 |-  ZZring
1 ccnfld 
 |-  CCfld
2 cress 
 |-  |`s
3 cz 
 |-  ZZ
4 1 3 2 co 
 |-  ( CCfld |`s ZZ )
5 0 4 wceq 
 |-  ZZring = ( CCfld |`s ZZ )