Theorem axicn

Description: _i is a complex number. Axiom 3 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn . (Contributed by NM, 23-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	axicn	⊢ i ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		0r	⊢ 0R ∈ R
2		1sr	⊢ 1R ∈ R
3		df-i	⊢ i = ⟨ 0R , 1R ⟩
4	3	eleq1i	⊢ ( i ∈ ℂ ↔ ⟨ 0R , 1R ⟩ ∈ ℂ )
5		opelcn	⊢ ( ⟨ 0R , 1R ⟩ ∈ ℂ ↔ ( 0R ∈ R ∧ 1R ∈ R ) )
6	4 5	bitri	⊢ ( i ∈ ℂ ↔ ( 0R ∈ R ∧ 1R ∈ R ) )
7	1 2 6	mpbir2an	⊢ i ∈ ℂ