Definition df-even

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

	Ref	Expression
Assertion	df-even	$$⊢\mathrm{Even}=\left\{z\in \mathbb{Z}|\frac{z}{2}\in \mathbb{Z}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceven	$$class\mathrm{Even}$$
1		vz	$$setvarz$$
2		cz	$$class\mathbb{Z}$$
3	1	cv	$$setvarz$$
4		cdiv	$$class÷$$
5		c2	$$class2$$
6	3 5 4	co	$$class\left(\frac{z}{2}\right)$$
7	6 2	wcel	$$wff\frac{z}{2}\in \mathbb{Z}$$
8	7 1 2	crab	$$class\left\{z\in \mathbb{Z}|\frac{z}{2}\in \mathbb{Z}\right\}$$
9	0 8	wceq	$$wff\mathrm{Even}=\left\{z\in \mathbb{Z}|\frac{z}{2}\in \mathbb{Z}\right\}$$