Theorem dfeven5

Description: Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020)

	Ref	Expression
Assertion	dfeven5	|- Even = { z e. ZZ | ( 2 gcd z ) = 2 }

Proof

Step	Hyp	Ref	Expression
1		iseven5	|- ( x e. Even <-> ( x e. ZZ /\ ( 2 gcd x ) = 2 ) )
2		oveq2	|- ( z = x -> ( 2 gcd z ) = ( 2 gcd x ) )
3	2	eqeq1d	|- ( z = x -> ( ( 2 gcd z ) = 2 <-> ( 2 gcd x ) = 2 ) )
4	3	elrab	|- ( x e. { z e. ZZ | ( 2 gcd z ) = 2 } <-> ( x e. ZZ /\ ( 2 gcd x ) = 2 ) )
5	1 4	bitr4i	|- ( x e. Even <-> x e. { z e. ZZ | ( 2 gcd z ) = 2 } )
6	5	eqriv	|- Even = { z e. ZZ | ( 2 gcd z ) = 2 }