ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-resscn GIF version

Axiom ax-resscn 7680
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7636. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 7587 . 2 class
2 cc 7586 . 2 class
31, 2wss 3041 1 wff ℝ ⊆ ℂ
Colors of variables: wff set class
This axiom is referenced by:  recn  7721  reex  7722  recni  7746  nnsscn  8689  nn0sscn  8940  qsscn  9379  reexpcl  10265  rpexpcl  10267  reexpclzap  10268  expge0  10284  expge1  10285  abscn2  11039  recn2  11041  imcn2  11042  climabs  11044  climre  11046  climim  11047  climcvg1nlem  11073  fsumrecl  11125  fsumrpcl  11128  fsumge0  11183  fsumre  11196  fsumim  11197  reeff1  11321  remet  12620  tgioo2cntop  12629  abscncf  12652  recncf  12653  imcncf  12654  cnrehmeocntop  12673  limcimolemlt  12713  recnprss  12736  dvcjbr  12752  dvfre  12754  cosz12  12772
  Copyright terms: Public domain W3C validator