Theorem iseven

Description: The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	|- ( z = Z -> ( z / 2 ) = ( Z / 2 ) )
2	1	eleq1d	|- ( z = Z -> ( ( z / 2 ) e. ZZ <-> ( Z / 2 ) e. ZZ ) )
3		df-even	|- Even = { z e. ZZ | ( z / 2 ) e. ZZ }
4	2 3	elrab2	|- ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )