This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax1cn

Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn . (Contributed by NM, 12-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax1cn	$⊢ 1 \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		axresscn	$⊢ ℝ \subseteq ℂ$
2		df-1	$⊢ 1 = ⟨1_{𝑹}, 0_{𝑹}⟩$
3		1sr	$⊢ 1_{𝑹} \in 𝑹$
4		opelreal	$⊢ ⟨1_{𝑹}, 0_{𝑹}⟩ \in ℝ \leftrightarrow 1_{𝑹} \in 𝑹$
5	3 4	mpbir	$⊢ ⟨1_{𝑹}, 0_{𝑹}⟩ \in ℝ$
6	2 5	eqeltri	$⊢ 1 \in ℝ$
7	1 6	sselii	$⊢ 1 \in ℂ$