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

Axiom ax-resscn 7033
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6993. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn  |-  RR  C_  CC

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 6945 . 2  class  RR
2 cc 6944 . 2  class  CC
31, 2wss 2944 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  7071  reex  7072  recni  7096  nnsscn  7994  nn0sscn  8243  qsscn  8662  serige0  9416  serile  9417  reexpcl  9436  rpexpcl  9438  reexpclzap  9439  expge0  9455  expge1  9456  abscn2  10065  recn2  10067  imcn2  10068  climabs  10070  climre  10072  climim  10073  iserile  10092  climserile  10095  climcvg1nlem  10098
  Copyright terms: Public domain W3C validator