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

Proof

Step	Hyp	Ref	Expression
1		axresscn	⊢ ℝ ⊆ ℂ
2		df-1	⊢ 1 = ⟨ 1R , 0R ⟩
3		1sr	⊢ 1R ∈ R
4		opelreal	⊢ ( ⟨ 1R , 0R ⟩ ∈ ℝ ↔ 1R ∈ R )
5	3 4	mpbir	⊢ ⟨ 1R , 0R ⟩ ∈ ℝ
6	2 5	eqeltri	⊢ 1 ∈ ℝ
7	1 6	sselii	⊢ 1 ∈ ℂ