This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfodd3

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

Ref Expression
Assertion dfodd3 
|- Odd = { z e. ZZ | -. 2 || z }

Proof

Step Hyp Ref Expression
1 dfodd6 
 |-  Odd = { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) }
2 eqcom 
 |-  ( z = ( ( 2 x. i ) + 1 ) <-> ( ( 2 x. i ) + 1 ) = z )
3 2 a1i 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( z = ( ( 2 x. i ) + 1 ) <-> ( ( 2 x. i ) + 1 ) = z ) )
4 3 rexbidva 
 |-  ( z e. ZZ -> ( E. i e. ZZ z = ( ( 2 x. i ) + 1 ) <-> E. i e. ZZ ( ( 2 x. i ) + 1 ) = z ) )
5 odd2np1 
 |-  ( z e. ZZ -> ( -. 2 || z <-> E. i e. ZZ ( ( 2 x. i ) + 1 ) = z ) )
6 4 5 bitr4d 
 |-  ( z e. ZZ -> ( E. i e. ZZ z = ( ( 2 x. i ) + 1 ) <-> -. 2 || z ) )
7 6 rabbiia 
 |-  { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) } = { z e. ZZ | -. 2 || z }
8 1 7 eqtri 
 |-  Odd = { z e. ZZ | -. 2 || z }