Theorem recni 8038

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 7971	. 2 ⊢ ℝ ⊆ ℂ
2		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
3	1, 2	sselii 3180	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2167  ℂcc 7877  ℝcr 7878

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7971

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  resubcli  8289  ltapii  8662  nncni  9000  2cn  9061  3cn  9065  4cn  9068  5cn  9070  6cn  9072  7cn  9074  8cn  9076  9cn  9078  halfcn  9205  8th4div3  9210  nn0cni  9261  numltc  9482  sqge0i  10718  lt2sqi  10719  le2sqi  10720  sq11i  10721  sqrtmsq2i  11300  0.999...  11686  ef01bndlem  11921  sin4lt0  11932  eirraplem  11942  eirr  11944  egt2lt3  11945  sqrt2irraplemnn  12347  modsubi  12588  picn  15023  sinhalfpilem  15027  cosneghalfpi  15034  sinhalfpip  15056  sinhalfpim  15057  coshalfpip  15058  coshalfpim  15059  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  cosq23lt0  15069  coseq00topi  15071  sincosq1eq  15075  sincos4thpi  15076  tan4thpi  15077  sincos6thpi  15078  2logb9irrALT  15210  taupi  15717