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