Theorem recni 7771

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

Syntax hints:   ∈ wcel 1480  ℂcc 7611  ℝcr 7612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-resscn 7705

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  resubcli  8018  ltapii  8390  nncni  8723  2cn  8784  3cn  8788  4cn  8791  5cn  8793  6cn  8795  7cn  8797  8cn  8799  9cn  8801  halfcn  8927  8th4div3  8932  nn0cni  8982  numltc  9200  sqge0i  10372  lt2sqi  10373  le2sqi  10374  sq11i  10375  sqrtmsq2i  10900  0.999...  11283  ef01bndlem  11452  sin4lt0  11462  eirraplem  11472  eirr  11474  egt2lt3  11475  sqrt2irraplemnn  11846  picn  12857  sinhalfpilem  12861  cosneghalfpi  12868  sinhalfpip  12890  sinhalfpim  12891  coshalfpip  12892  coshalfpim  12893  sincosq1sgn  12896  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  cosq23lt0  12903  coseq00topi  12905  sincosq1eq  12909  sincos4thpi  12910  tan4thpi  12911  sincos6thpi  12912  taupi  13228