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

Axiom ax-resscn 7534
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7494. (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 7446 . 2  class  RR
2 cc 7445 . 2  class  CC
31, 2wss 3013 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  7572  reex  7573  recni  7597  nnsscn  8525  nn0sscn  8776  qsscn  9215  reexpcl  10087  rpexpcl  10089  reexpclzap  10090  expge0  10106  expge1  10107  abscn2  10858  recn2  10860  imcn2  10861  climabs  10863  climre  10865  climim  10866  climcvg1nlem  10892  fsumrecl  10944  fsumrpcl  10947  fsumge0  11002  fsumre  11015  fsumim  11016  reeff1  11140  remet  12314  abscncf  12338  recncf  12339  imcncf  12340
  Copyright terms: Public domain W3C validator