Theorem dfodd3

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

	Ref	Expression
Assertion	dfodd3	|- Odd = { z e. ZZ | -. 2 || z }

Proof

Step	Hyp	Ref	Expression
1		dfodd6	|- Odd = { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) }
2		eqcom	|- ( z = ( ( 2 x. i ) + 1 ) <-> ( ( 2 x. i ) + 1 ) = z )
3	2	a1i	|- ( ( z e. ZZ /\ i e. ZZ ) -> ( z = ( ( 2 x. i ) + 1 ) <-> ( ( 2 x. i ) + 1 ) = z ) )
4	3	rexbidva	|- ( z e. ZZ -> ( E. i e. ZZ z = ( ( 2 x. i ) + 1 ) <-> E. i e. ZZ ( ( 2 x. i ) + 1 ) = z ) )
5		odd2np1	|- ( z e. ZZ -> ( -. 2 || z <-> E. i e. ZZ ( ( 2 x. i ) + 1 ) = z ) )
6	4 5	bitr4d	|- ( z e. ZZ -> ( E. i e. ZZ z = ( ( 2 x. i ) + 1 ) <-> -. 2 || z ) )
7	6	rabbiia	|- { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) } = { z e. ZZ | -. 2 || z }
8	1 7	eqtri	|- Odd = { z e. ZZ | -. 2 || z }