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 ℂ$$