Definition df-even 44694

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

Assertion

Ref	Expression
df-even	⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}

Detailed syntax breakdown of Definition df-even

Step	Hyp	Ref	Expression
1		ceven 44692	. 2 class Even
2		vz	. . . . . 6 setvar 𝑧
3	2	cv 1542	. . . . 5 class 𝑧
4		c2 11850	. . . . 5 class 2
5		cdiv 11454	. . . . 5 class /
6	3, 4, 5	co 7191	. . . 4 class (𝑧 / 2)
7		cz 12141	. . . 4 class ℤ
8	6, 7	wcel 2112	. . 3 wff (𝑧 / 2) ∈ ℤ
9	8, 2, 7	crab 3055	. 2 class {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
10	1, 9	wceq 1543	1 wff Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}

This definition is referenced by:  iseven  44696  dfeven4  44706  dfeven3  44726