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

Metamath Proof Explorer

Theorem 0ncn

Description: The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by NM, 2-May-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	0ncn	⊢ ¬ ∅ ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		0nelxp	⊢ ¬ ∅ ∈ ( R × R )
2		df-c	⊢ ℂ = ( R × R )
3	2	eleq2i	⊢ ( ∅ ∈ ℂ ↔ ∅ ∈ ( R × R ) )
4	1 3	mtbir	⊢ ¬ ∅ ∈ ℂ