Theorem recni 7983

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

Syntax hints:   ∈ wcel 2158  ℂcc 7823  ℝcr 7824

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-resscn 7917

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  resubcli  8234  ltapii  8606  nncni  8943  2cn  9004  3cn  9008  4cn  9011  5cn  9013  6cn  9015  7cn  9017  8cn  9019  9cn  9021  halfcn  9147  8th4div3  9152  nn0cni  9202  numltc  9423  sqge0i  10621  lt2sqi  10622  le2sqi  10623  sq11i  10624  sqrtmsq2i  11158  0.999...  11543  ef01bndlem  11778  sin4lt0  11788  eirraplem  11798  eirr  11800  egt2lt3  11801  sqrt2irraplemnn  12193  picn  14504  sinhalfpilem  14508  cosneghalfpi  14515  sinhalfpip  14537  sinhalfpim  14538  coshalfpip  14539  coshalfpim  14540  sincosq1sgn  14543  sincosq2sgn  14544  sincosq3sgn  14545  sincosq4sgn  14546  cosq23lt0  14550  coseq00topi  14552  sincosq1eq  14556  sincos4thpi  14557  tan4thpi  14558  sincos6thpi  14559  2logb9irrALT  14688  taupi  15118