2even

		Ref	Expression
	Hypothesis	2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
	Assertion	2even	$⊢ 2 \in E$

Step	Hyp	Ref	Expression
1		2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
2		2z	$⊢ 2 \in ℤ$
3		2cn	$⊢ 2 \in ℂ$
4		1zzd	$⊢ 2 \in ℂ \to 1 \in ℤ$
5		oveq2	$⊢ x = 1 \to 2 x = 2 \cdot 1$
6	5	eqeq2d	$⊢ x = 1 \to (2 = 2 x \leftrightarrow 2 = 2 \cdot 1)$
7	6	adantl	$⊢ (2 \in ℂ \land x = 1) \to (2 = 2 x \leftrightarrow 2 = 2 \cdot 1)$
8		mulid1	$⊢ 2 \in ℂ \to 2 \cdot 1 = 2$
9	8	eqcomd	$⊢ 2 \in ℂ \to 2 = 2 \cdot 1$
10	4 7 9	rspcedvd	$⊢ 2 \in ℂ \to \exists x \in ℤ 2 = 2 x$
11	3 10	ax-mp	$⊢ \exists x \in ℤ 2 = 2 x$
12		eqeq1	$⊢ z = 2 \to (z = 2 x \leftrightarrow 2 = 2 x)$
13	12	rexbidv	$⊢ z = 2 \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ 2 = 2 x)$
14	13	elrab	$⊢ 2 \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \leftrightarrow (2 \in ℤ \land \exists x \in ℤ 2 = 2 x)$
15	2 11 14	mpbir2an	$⊢ 2 \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
16	15 1	eleqtrri	$⊢ 2 \in E$

Metamath Proof Explorer