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

Axiom ax-resscn 7384
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7344. (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 7296 . 2  class  RR
2 cc 7295 . 2  class  CC
31, 2wss 2988 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  7422  reex  7423  recni  7447  nnsscn  8365  nn0sscn  8614  qsscn  9051  serige0  9854  serile  9855  reexpcl  9874  rpexpcl  9876  reexpclzap  9877  expge0  9893  expge1  9894  abscn2  10600  recn2  10602  imcn2  10603  climabs  10605  climre  10607  climim  10608  iserile  10627  climserile  10630  climcvg1nlem  10633  fsumrecl  10683  fsumrpcl  10686
  Copyright terms: Public domain W3C validator