Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > recni | GIF version |
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
recni.1 | ⊢ 𝐴 ∈ ℝ |
Ref | Expression |
---|---|
recni | ⊢ 𝐴 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-resscn 6976 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | recni.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
3 | 1, 2 | sselii 2942 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1393 ℂcc 6887 ℝcr 6888 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-resscn 6976 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-in 2924 df-ss 2931 |
This theorem is referenced by: resubcli 7274 ltapii 7624 nncni 7924 2cn 7986 3cn 7990 4cn 7993 5cn 7995 6cn 7997 7cn 7999 8cn 8001 9cn 8003 halfcn 8139 8th4div3 8144 nn0cni 8193 numltc 8387 sqge0i 9340 lt2sqi 9341 le2sqi 9342 sq11i 9343 sqrtmsq2i 9731 |
Copyright terms: Public domain | W3C validator |