Definition df-zring

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

	Ref	Expression
Assertion	df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		zring	$$class{\mathbb{Z}}_{\mathrm{ring}}$$
1		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
2		cress	$$class{\upharpoonright }_{𝑠}$$
3		cz	$$class\mathbb{Z}$$
4	1 3 2	co	$$class\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)$$
5	0 4	wceq	$$wff{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$