Theorem recni 7944

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

Syntax hints:   ∈ wcel 2146  ℂcc 7784  ℝcr 7785

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-resscn 7878

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  resubcli  8194  ltapii  8566  nncni  8900  2cn  8961  3cn  8965  4cn  8968  5cn  8970  6cn  8972  7cn  8974  8cn  8976  9cn  8978  halfcn  9104  8th4div3  9109  nn0cni  9159  numltc  9380  sqge0i  10574  lt2sqi  10575  le2sqi  10576  sq11i  10577  sqrtmsq2i  11110  0.999...  11495  ef01bndlem  11730  sin4lt0  11740  eirraplem  11750  eirr  11752  egt2lt3  11753  sqrt2irraplemnn  12144  picn  13759  sinhalfpilem  13763  cosneghalfpi  13770  sinhalfpip  13792  sinhalfpim  13793  coshalfpip  13794  coshalfpim  13795  sincosq1sgn  13798  sincosq2sgn  13799  sincosq3sgn  13800  sincosq4sgn  13801  cosq23lt0  13805  coseq00topi  13807  sincosq1eq  13811  sincos4thpi  13812  tan4thpi  13813  sincos6thpi  13814  2logb9irrALT  13943  taupi  14359