Theorem recni 7229

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

Syntax hints:   ∈ wcel 1434  ℂcc 7077  ℝcr 7078

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-resscn 7166

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2989  df-ss 2996

This theorem is referenced by:  resubcli  7474  ltapii  7836  nncni  8152  2cn  8213  3cn  8217  4cn  8220  5cn  8222  6cn  8224  7cn  8226  8cn  8228  9cn  8230  halfcn  8348  8th4div3  8353  nn0cni  8403  numltc  8619  sqge0i  9695  lt2sqi  9696  le2sqi  9697  sq11i  9698  sqrtmsq2i  10206  sqrt2irraplemnn  10748