Theorem recni 8191

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

Syntax hints:   ∈ wcel 2202  ℂcc 8030  ℝcr 8031

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  resubcli  8442  ltapii  8815  nncni  9153  2cn  9214  3cn  9218  4cn  9221  5cn  9223  6cn  9225  7cn  9227  8cn  9229  9cn  9231  halfcn  9358  8th4div3  9363  nn0cni  9414  numltc  9636  sqge0i  10889  lt2sqi  10890  le2sqi  10891  sq11i  10892  sqrtmsq2i  11700  0.999...  12087  ef01bndlem  12322  sin4lt0  12333  eirraplem  12343  eirr  12345  egt2lt3  12346  sqrt2irraplemnn  12756  modsubi  12997  picn  15517  sinhalfpilem  15521  cosneghalfpi  15528  sinhalfpip  15550  sinhalfpim  15551  coshalfpip  15552  coshalfpim  15553  sincosq1sgn  15556  sincosq2sgn  15557  sincosq3sgn  15558  sincosq4sgn  15559  cosq23lt0  15563  coseq00topi  15565  sincosq1eq  15569  sincos4thpi  15570  tan4thpi  15571  sincos6thpi  15572  2logb9irrALT  15704  taupi  16703