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

Axiom ax-resscn 7034
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6994. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 6946 . 2 class
2 cc 6945 . 2 class
31, 2wss 2945 1 wff ℝ ⊆ ℂ
Colors of variables: wff set class
This axiom is referenced by:  recn  7072  reex  7073  recni  7097  nnsscn  7995  nn0sscn  8244  qsscn  8663  serige0  9417  serile  9418  reexpcl  9437  rpexpcl  9439  reexpclzap  9440  expge0  9456  expge1  9457  abscn2  10066  recn2  10068  imcn2  10069  climabs  10071  climre  10073  climim  10074  iserile  10093  climserile  10096  climcvg1nlem  10099
  Copyright terms: Public domain W3C validator