Theorem recni 8234

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

Syntax hints:   ∈ wcel 2202  ℂcc 8073  ℝcr 8074

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  resubcli  8485  ltapii  8858  nncni  9196  2cn  9257  3cn  9261  4cn  9264  5cn  9266  6cn  9268  7cn  9270  8cn  9272  9cn  9274  halfcn  9401  8th4div3  9406  nn0cni  9457  numltc  9679  sqge0i  10932  lt2sqi  10933  le2sqi  10934  sq11i  10935  sqrtmsq2i  11756  0.999...  12143  ef01bndlem  12378  sin4lt0  12389  eirraplem  12399  eirr  12401  egt2lt3  12402  sqrt2irraplemnn  12812  modsubi  13053  picn  15578  sinhalfpilem  15582  cosneghalfpi  15589  sinhalfpip  15611  sinhalfpim  15612  coshalfpip  15613  coshalfpim  15614  sincosq1sgn  15617  sincosq2sgn  15618  sincosq3sgn  15619  sincosq4sgn  15620  cosq23lt0  15624  coseq00topi  15626  sincosq1eq  15630  sincos4thpi  15631  tan4thpi  15632  sincos6thpi  15633  2logb9irrALT  15765  taupi  16786