Theorem recni 7696

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

Syntax hints:   ∈ wcel 1461  ℂcc 7539  ℝcr 7540

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-resscn 7631

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-in 3041  df-ss 3048

This theorem is referenced by:  resubcli  7942  ltapii  8308  nncni  8634  2cn  8695  3cn  8699  4cn  8702  5cn  8704  6cn  8706  7cn  8708  8cn  8710  9cn  8712  halfcn  8832  8th4div3  8837  nn0cni  8887  numltc  9105  sqge0i  10266  lt2sqi  10267  le2sqi  10268  sq11i  10269  sqrtmsq2i  10793  0.999...  11176  ef01bndlem  11308  sin4lt0  11318  eirraplem  11325  eirr  11327  egt2lt3  11328  sqrt2irraplemnn  11696