Metamath Proof Explorer

Theorem dfodd2

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

Ref Expression
Assertion dfodd2 ⊢ Odd = z ∈ ℤ | z − 1 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 isodd2 ⊢ x ∈ Odd ↔ x ∈ ℤ ∧ x − 1 2 ∈ ℤ
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 ∈ ℤ ↔ x − 1 2 ∈ ℤ
5 4 elrab ⊢ x ∈ z ∈ ℤ | z − 1 2 ∈ ℤ ↔ x ∈ ℤ ∧ x − 1 2 ∈ ℤ
6 1 5 bitr4i ⊢ x ∈ Odd ↔ x ∈ z ∈ ℤ | z − 1 2 ∈ ℤ
7 6 eqriv ⊢ Odd = z ∈ ℤ | z − 1 2 ∈ ℤ