Definition df-za

Description: Define an algebraic integer as a complex number which is the root of a monic integer polynomial. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Assertion	df-za	⊢ ℤ = ( IntgOver ‘ ℤ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cza	⊢ ℤ
1		citgo	⊢ IntgOver
2		cz	⊢ ℤ
3	2 1	cfv	⊢ ( IntgOver ‘ ℤ )
4	0 3	wceq	⊢ ℤ = ( IntgOver ‘ ℤ )