Theorem recni 8302

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

Hypothesis

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ

Assertion

Ref	Expression
recni	⊢ 𝐴 ∈ ℂ

Proof of Theorem recni

Step	Hyp	Ref	Expression
1		ax-resscn 8235	. 2 ⊢ ℝ ⊆ ℂ
2		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
3	1, 2	sselii 3239	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2205  ℂcc 8141  ℝcr 8142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  resubcli  8553  ltapii  8927  nncni  9267  2cn  9328  3cn  9332  4cn  9335  5cn  9337  6cn  9339  7cn  9341  8cn  9343  9cn  9345  halfcn  9472  8th4div3  9477  nn0cni  9528  numltc  9755  sqge0i  11015  lt2sqi  11016  le2sqi  11017  sq11i  11018  sqrtmsq2i  11849  0.999...  12236  ef01bndlem  12471  sin4lt0  12482  eirraplem  12492  eirr  12494  egt2lt3  12495  sqrt2irraplemnn  12905  modsubi  13146  picn  15782  sinhalfpilem  15786  cosneghalfpi  15793  sinhalfpip  15815  sinhalfpim  15816  coshalfpip  15817  coshalfpim  15818  sincosq1sgn  15821  sincosq2sgn  15822  sincosq3sgn  15823  sincosq4sgn  15824  cosq23lt0  15828  coseq00topi  15830  sincosq1eq  15834  sincos4thpi  15835  tan4thpi  15836  sincos6thpi  15837  2logb9irrALT  15969  taupi  16998