Theorem dfodd2

Description: Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020)

	Ref	Expression
Assertion	dfodd2	|- Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ }

Proof

Step	Hyp	Ref	Expression
1		isodd2	|- ( x e. Odd <-> ( x e. ZZ /\ ( ( x - 1 ) / 2 ) e. ZZ ) )
2		oveq1	|- ( z = x -> ( z - 1 ) = ( x - 1 ) )
3	2	oveq1d	|- ( z = x -> ( ( z - 1 ) / 2 ) = ( ( x - 1 ) / 2 ) )
4	3	eleq1d	|- ( z = x -> ( ( ( z - 1 ) / 2 ) e. ZZ <-> ( ( x - 1 ) / 2 ) e. ZZ ) )
5	4	elrab	|- ( x e. { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ } <-> ( x e. ZZ /\ ( ( x - 1 ) / 2 ) e. ZZ ) )
6	1 5	bitr4i	|- ( x e. Odd <-> x e. { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ } )
7	6	eqriv	|- Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ }