Definition df-even 41539

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

Assertion

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

Detailed syntax breakdown of Definition df-even

Step	Hyp	Ref	Expression
1		ceven 41537	. 2 class Even
2		vz	. . . . . 6 setvar z
3	2	cv 1482	. . . . 5 class z
4		c2 11070	. . . . 5 class 2
5		cdiv 10684	. . . . 5 class /
6	3, 4, 5	co 6650	. . . 4 class ( z / 2 )
7		cz 11377	. . . 4 class ZZ
8	6, 7	wcel 1990	. . 3 wff ( z / 2 ) e. ZZ
9	8, 2, 7	crab 2916	. 2 class { z e. ZZ | ( z / 2 ) e. ZZ }
10	1, 9	wceq 1483	1 wff Even = { z e. ZZ | ( z / 2 ) e. ZZ }

This definition is referenced by:  iseven  41541  dfeven4  41551  dfeven3  41570