Theorem recni 7131

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

Hypothesis

Ref	Expression
recni.1	|- A e. RR

Assertion

Ref	Expression
recni	|- A e. CC

Proof of Theorem recni

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

Syntax hints:   e. wcel 1433   CCcc 6979   RRcr 6980

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986

This theorem is referenced by:  resubcli  7371  ltapii  7733  nncni  8049  2cn  8110  3cn  8114  4cn  8117  5cn  8119  6cn  8121  7cn  8123  8cn  8125  9cn  8127  halfcn  8245  8th4div3  8250  nn0cni  8300  numltc  8502  sqge0i  9562  lt2sqi  9563  le2sqi  9564  sq11i  9565  sqrtmsq2i  10021  sqrt2irraplemnn  10557