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