Theorem recni 7969

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

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

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 7903

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 3136  df-ss 3143

This theorem is referenced by:  resubcli  8220  ltapii  8592  nncni  8929  2cn  8990  3cn  8994  4cn  8997  5cn  8999  6cn  9001  7cn  9003  8cn  9005  9cn  9007  halfcn  9133  8th4div3  9138  nn0cni  9188  numltc  9409  sqge0i  10607  lt2sqi  10608  le2sqi  10609  sq11i  10610  sqrtmsq2i  11144  0.999...  11529  ef01bndlem  11764  sin4lt0  11774  eirraplem  11784  eirr  11786  egt2lt3  11787  sqrt2irraplemnn  12179  picn  14211  sinhalfpilem  14215  cosneghalfpi  14222  sinhalfpip  14244  sinhalfpim  14245  coshalfpip  14246  coshalfpim  14247  sincosq1sgn  14250  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  cosq23lt0  14257  coseq00topi  14259  sincosq1eq  14263  sincos4thpi  14264  tan4thpi  14265  sincos6thpi  14266  2logb9irrALT  14395  taupi  14823