Theorem dfodd7

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

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

Proof

Step	Hyp	Ref	Expression
1		isodd7	|- ( x e. Odd <-> ( x e. ZZ /\ ( 2 gcd x ) = 1 ) )
2		oveq2	|- ( z = x -> ( 2 gcd z ) = ( 2 gcd x ) )
3	2	eqeq1d	|- ( z = x -> ( ( 2 gcd z ) = 1 <-> ( 2 gcd x ) = 1 ) )
4	3	elrab	|- ( x e. { z e. ZZ | ( 2 gcd z ) = 1 } <-> ( x e. ZZ /\ ( 2 gcd x ) = 1 ) )
5	1 4	bitr4i	|- ( x e. Odd <-> x e. { z e. ZZ | ( 2 gcd z ) = 1 } )
6	5	eqriv	|- Odd = { z e. ZZ | ( 2 gcd z ) = 1 }