Definition df-even

Description: Define the set of even numbers. (Contributed by AV, 14-Jun-2020)

	Ref	Expression
Assertion	df-even	|- Even = { z e. ZZ | ( z / 2 ) e. ZZ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceven	|- Even
1		vz	|- z
2		cz	|- ZZ
3	1	cv	|- z
4		cdiv	|- /
5		c2	|- 2
6	3 5 4	co	|- ( z / 2 )
7	6 2	wcel	|- ( z / 2 ) e. ZZ
8	7 1 2	crab	|- { z e. ZZ | ( z / 2 ) e. ZZ }
9	0 8	wceq	|- Even = { z e. ZZ | ( z / 2 ) e. ZZ }