Metamath Proof Explorer

Theorem recni

Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995)

Ref Expression
Hypothesis recni.1 
|- A e. RR
Assertion recni 
|- A e. CC

Proof

Step Hyp Ref Expression
1 recni.1 
 |-  A e. RR
2 ax-resscn 
 |-  RR C_ CC
3 2 1 sselii 
 |-  A e. CC