Metamath Proof Explorer


Theorem dfodd3

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

Ref Expression
Assertion dfodd3 Odd=z|¬2z

Proof

Step Hyp Ref Expression
1 dfodd6 Odd=z|iz=2i+1
2 eqcom z=2i+12i+1=z
3 2 a1i ziz=2i+12i+1=z
4 3 rexbidva ziz=2i+1i2i+1=z
5 odd2np1 z¬2zi2i+1=z
6 4 5 bitr4d ziz=2i+1¬2z
7 6 rabbiia z|iz=2i+1=z|¬2z
8 1 7 eqtri Odd=z|¬2z