Theorem dfeven5

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

	Ref	Expression
Assertion	dfeven5	$$⊢\mathrm{Even}=\left\{z\in \mathbb{Z}|2\gcd z=2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		iseven5	$$⊢x\in \mathrm{Even}\leftrightarrow \left(x\in \mathbb{Z}\wedge 2\gcd x=2\right)$$
2		oveq2	$$⊢z=x\to 2\gcd z=2\gcd x$$
3	2	eqeq1d	$$⊢z=x\to \left(2\gcd z=2\leftrightarrow 2\gcd x=2\right)$$
4	3	elrab	$$⊢x\in \left\{z\in \mathbb{Z}|2\gcd z=2\right\}\leftrightarrow \left(x\in \mathbb{Z}\wedge 2\gcd x=2\right)$$
5	1 4	bitr4i	$$⊢x\in \mathrm{Even}\leftrightarrow x\in \left\{z\in \mathbb{Z}|2\gcd z=2\right\}$$
6	5	eqriv	$$⊢\mathrm{Even}=\left\{z\in \mathbb{Z}|2\gcd z=2\right\}$$