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 ring = fld 𝑠

Detailed syntax breakdown

Step Hyp Ref Expression
0 zring class ring
1 ccnfld class fld
2 cress class 𝑠
3 cz class
4 1 3 2 co class fld 𝑠
5 0 4 wceq wff ring = fld 𝑠