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

Metamath Proof Explorer

Definition df-odd

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

Ref Expression
Assertion df-odd ⊢ Odd = z ∈ ℤ | z + 1 2 ∈ ℤ

Detailed syntax breakdown

Step Hyp Ref Expression
0 codd class Odd
1 vz setvar z
2 cz class ℤ
3 1 cv setvar z
4 caddc class +
5 c1 class 1
6 3 5 4 co class z + 1
7 cdiv class ÷
8 c2 class 2
9 6 8 7 co class z + 1 2
10 9 2 wcel wff z + 1 2 ∈ ℤ
11 10 1 2 crab class z ∈ ℤ | z + 1 2 ∈ ℤ
12 0 11 wceq wff Odd = z ∈ ℤ | z + 1 2 ∈ ℤ