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

Axiom ax-resscn 7200
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7160. (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 7112 . 2  class  RR
2 cc 7111 . 2  class  CC
31, 2wss 2982 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  7238  reex  7239  recni  7263  nnsscn  8181  nn0sscn  8430  qsscn  8867  serige0  9640  serile  9641  reexpcl  9660  rpexpcl  9662  reexpclzap  9663  expge0  9679  expge1  9680  abscn2  10372  recn2  10374  imcn2  10375  climabs  10377  climre  10379  climim  10380  iserile  10399  climserile  10402  climcvg1nlem  10405
  Copyright terms: Public domain W3C validator