Theorem dfodd7

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

	Ref	Expression
Assertion	dfodd7	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 1 }

Proof

Step	Hyp	Ref	Expression
1		isodd7	⊢ ( 𝑥 ∈ Odd ↔ ( 𝑥 ∈ ℤ ∧ ( 2 gcd 𝑥 ) = 1 ) )
2		oveq2	⊢ ( 𝑧 = 𝑥 → ( 2 gcd 𝑧 ) = ( 2 gcd 𝑥 ) )
3	2	eqeq1d	⊢ ( 𝑧 = 𝑥 → ( ( 2 gcd 𝑧 ) = 1 ↔ ( 2 gcd 𝑥 ) = 1 ) )
4	3	elrab	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 1 } ↔ ( 𝑥 ∈ ℤ ∧ ( 2 gcd 𝑥 ) = 1 ) )
5	1 4	bitr4i	⊢ ( 𝑥 ∈ Odd ↔ 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 1 } )
6	5	eqriv	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 1 }