Theorem dfodd5

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

	Ref	Expression
Assertion	dfodd5	|- Odd = { z e. ZZ | ( z mod 2 ) =/= 0 }

Proof

Step	Hyp	Ref	Expression
1		dfodd4	|- Odd = { z e. ZZ | ( z mod 2 ) = 1 }
2		elmod2	|- ( z e. ZZ -> ( z mod 2 ) e. { 0 , 1 } )
3		prcom	|- { 0 , 1 } = { 1 , 0 }
4	3	eleq2i	|- ( ( z mod 2 ) e. { 0 , 1 } <-> ( z mod 2 ) e. { 1 , 0 } )
5	4	biimpi	|- ( ( z mod 2 ) e. { 0 , 1 } -> ( z mod 2 ) e. { 1 , 0 } )
6		ax-1ne0	|- 1 =/= 0
7		elprneb	|- ( ( ( z mod 2 ) e. { 1 , 0 } /\ 1 =/= 0 ) -> ( ( z mod 2 ) = 1 <-> ( z mod 2 ) =/= 0 ) )
8	5 6 7	sylancl	|- ( ( z mod 2 ) e. { 0 , 1 } -> ( ( z mod 2 ) = 1 <-> ( z mod 2 ) =/= 0 ) )
9	2 8	syl	|- ( z e. ZZ -> ( ( z mod 2 ) = 1 <-> ( z mod 2 ) =/= 0 ) )
10	9	rabbiia	|- { z e. ZZ | ( z mod 2 ) = 1 } = { z e. ZZ | ( z mod 2 ) =/= 0 }
11	1 10	eqtri	|- Odd = { z e. ZZ | ( z mod 2 ) =/= 0 }