Theorem recni 8166

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

Syntax hints:   ∈ wcel 2200  ℂcc 8005  ℝcr 8006

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8099

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  resubcli  8417  ltapii  8790  nncni  9128  2cn  9189  3cn  9193  4cn  9196  5cn  9198  6cn  9200  7cn  9202  8cn  9204  9cn  9206  halfcn  9333  8th4div3  9338  nn0cni  9389  numltc  9611  sqge0i  10856  lt2sqi  10857  le2sqi  10858  sq11i  10859  sqrtmsq2i  11654  0.999...  12040  ef01bndlem  12275  sin4lt0  12286  eirraplem  12296  eirr  12298  egt2lt3  12299  sqrt2irraplemnn  12709  modsubi  12950  picn  15469  sinhalfpilem  15473  cosneghalfpi  15480  sinhalfpip  15502  sinhalfpim  15503  coshalfpip  15504  coshalfpim  15505  sincosq1sgn  15508  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  cosq23lt0  15515  coseq00topi  15517  sincosq1eq  15521  sincos4thpi  15522  tan4thpi  15523  sincos6thpi  15524  2logb9irrALT  15656  taupi  16471