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  8552  ltapii  8926  nncni  9264  2cn  9325  3cn  9329  4cn  9332  5cn  9334  6cn  9336  7cn  9338  8cn  9340  9cn  9342  halfcn  9469  8th4div3  9474  nn0cni  9525  numltc  9752  sqge0i  11012  lt2sqi  11013  le2sqi  11014  sq11i  11015  sqrtmsq2i  11845  0.999...  12232  ef01bndlem  12467  sin4lt0  12478  eirraplem  12488  eirr  12490  egt2lt3  12491  sqrt2irraplemnn  12901  modsubi  13142  picn  15764  sinhalfpilem  15768  cosneghalfpi  15775  sinhalfpip  15797  sinhalfpim  15798  coshalfpip  15799  coshalfpim  15800  sincosq1sgn  15803  sincosq2sgn  15804  sincosq3sgn  15805  sincosq4sgn  15806  cosq23lt0  15810  coseq00topi  15812  sincosq1eq  15816  sincos4thpi  15817  tan4thpi  15818  sincos6thpi  15819  2logb9irrALT  15951  taupi  16971