Metamath Proof Explorer

Theorem iseven2

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

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

Proof

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