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

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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 7540 . 2 class
2 cc 7539 . 2 class
31, 2wss 3035 1 wff ℝ ⊆ ℂ
Colors of variables: wff set class
This axiom is referenced by:  recn  7671  reex  7672  recni  7696  nnsscn  8629  nn0sscn  8880  qsscn  9319  reexpcl  10197  rpexpcl  10199  reexpclzap  10200  expge0  10216  expge1  10217  abscn2  10970  recn2  10972  imcn2  10973  climabs  10975  climre  10977  climim  10978  climcvg1nlem  11004  fsumrecl  11056  fsumrpcl  11059  fsumge0  11114  fsumre  11127  fsumim  11128  reeff1  11252  remet  12520  tgioo2cntop  12529  abscncf  12552  recncf  12553  imcncf  12554  limcimolemlt  12583  recnprss  12605
  Copyright terms: Public domain W3C validator