Theorem dfeven5

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

	Ref	Expression
Assertion	dfeven5	⊢ Even = { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 2 }

Proof

Step	Hyp	Ref	Expression
1		iseven5	⊢ ( 𝑥 ∈ Even ↔ ( 𝑥 ∈ ℤ ∧ ( 2 gcd 𝑥 ) = 2 ) )
2		oveq2	⊢ ( 𝑧 = 𝑥 → ( 2 gcd 𝑧 ) = ( 2 gcd 𝑥 ) )
3	2	eqeq1d	⊢ ( 𝑧 = 𝑥 → ( ( 2 gcd 𝑧 ) = 2 ↔ ( 2 gcd 𝑥 ) = 2 ) )
4	3	elrab	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 2 } ↔ ( 𝑥 ∈ ℤ ∧ ( 2 gcd 𝑥 ) = 2 ) )
5	1 4	bitr4i	⊢ ( 𝑥 ∈ Even ↔ 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 2 } )
6	5	eqriv	⊢ Even = { 𝑧 ∈ ℤ ∣ ( 2 gcd 𝑧 ) = 2 }