Theorem recni 7968

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

Syntax hints:   ∈ wcel 2148  ℂcc 7808  ℝcr 7809

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  resubcli  8219  ltapii  8591  nncni  8928  2cn  8989  3cn  8993  4cn  8996  5cn  8998  6cn  9000  7cn  9002  8cn  9004  9cn  9006  halfcn  9132  8th4div3  9137  nn0cni  9187  numltc  9408  sqge0i  10606  lt2sqi  10607  le2sqi  10608  sq11i  10609  sqrtmsq2i  11143  0.999...  11528  ef01bndlem  11763  sin4lt0  11773  eirraplem  11783  eirr  11785  egt2lt3  11786  sqrt2irraplemnn  12178  picn  14178  sinhalfpilem  14182  cosneghalfpi  14189  sinhalfpip  14211  sinhalfpim  14212  coshalfpip  14213  coshalfpim  14214  sincosq1sgn  14217  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  cosq23lt0  14224  coseq00topi  14226  sincosq1eq  14230  sincos4thpi  14231  tan4thpi  14232  sincos6thpi  14233  2logb9irrALT  14362  taupi  14790