Metamath Proof Explorer

Theorem dfodd3

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

Ref Expression
Assertion dfodd3 ⊢ Odd = z ∈ ℤ | ¬ 2 ∥ z

Proof

Step Hyp Ref Expression
1 dfodd6 ⊢ Odd = z ∈ ℤ | ∃ i ∈ ℤ z = 2 ⁢ i + 1
2 eqcom ⊢ z = 2 ⁢ i + 1 ↔ 2 ⁢ i + 1 = z
3 2 a1i ⊢ z ∈ ℤ ∧ i ∈ ℤ → z = 2 ⁢ i + 1 ↔ 2 ⁢ i + 1 = z
4 3 rexbidva ⊢ z ∈ ℤ → ∃ i ∈ ℤ z = 2 ⁢ i + 1 ↔ ∃ i ∈ ℤ 2 ⁢ i + 1 = z
5 odd2np1 ⊢ z ∈ ℤ → ¬ 2 ∥ z ↔ ∃ i ∈ ℤ 2 ⁢ i + 1 = z
6 4 5 bitr4d ⊢ z ∈ ℤ → ∃ i ∈ ℤ z = 2 ⁢ i + 1 ↔ ¬ 2 ∥ z
7 6 rabbiia ⊢ z ∈ ℤ | ∃ i ∈ ℤ z = 2 ⁢ i + 1 = z ∈ ℤ | ¬ 2 ∥ z
8 1 7 eqtri ⊢ Odd = z ∈ ℤ | ¬ 2 ∥ z