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 ↾s ℤ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		zring	⊢ ℤring
1		ccnfld	⊢ ℂfld
2		cress	⊢ ↾s
3		cz	⊢ ℤ
4	1 3 2	co	⊢ ( ℂfld ↾s ℤ )
5	0 4	wceq	⊢ ℤring = ( ℂfld ↾s ℤ )