Metamath Proof Explorer

Theorem isodd3

Description: The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion isodd3 
|- ( Z e. Odd <-> ( Z e. ZZ /\ -. 2 || Z ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( z = Z -> ( 2 || z <-> 2 || Z ) )
2 1 notbid 
 |-  ( z = Z -> ( -. 2 || z <-> -. 2 || Z ) )
3 dfodd3 
 |-  Odd = { z e. ZZ | -. 2 || z }
4 2 3 elrab2 
 |-  ( Z e. Odd <-> ( Z e. ZZ /\ -. 2 || Z ) )