Definition df-even

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceven	⊢ Even
1		vz	⊢ 𝑧
2		cz	⊢ ℤ
3	1	cv	⊢ 𝑧
4		cdiv	⊢ /
5		c2	⊢ 2
6	3 5 4	co	⊢ ( 𝑧 / 2 )
7	6 2	wcel	⊢ ( 𝑧 / 2 ) ∈ ℤ
8	7 1 2	crab	⊢ { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ }
9	0 8	wceq	⊢ Even = { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ }