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

Axiom ax-resscn 7705
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7661. (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 7612 . 2  class  RR
2 cc 7611 . 2  class  CC
31, 2wss 3066 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  7746  reex  7747  recni  7771  nnsscn  8718  nn0sscn  8975  qsscn  9416  reexpcl  10303  rpexpcl  10305  reexpclzap  10306  expge0  10322  expge1  10323  abscn2  11077  recn2  11079  imcn2  11080  climabs  11082  climre  11084  climim  11085  climcvg1nlem  11111  fsumrecl  11163  fsumrpcl  11166  fsumge0  11221  fsumre  11234  fsumim  11235  reeff1  11396  remet  12698  tgioo2cntop  12707  abscncf  12730  recncf  12731  imcncf  12732  cnrehmeocntop  12751  limcimolemlt  12791  recnprss  12814  dvcjbr  12830  dvfre  12832  cosz12  12850
  Copyright terms: Public domain W3C validator