This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∈ ℤ }