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

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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 6888 . 2 class
2 cc 6887 . 2 class
31, 2wss 2917 1 wff ℝ ⊆ ℂ
Colors of variables: wff set class
This axiom is referenced by:  recn  7014  reex  7015  recni  7039  nnsscn  7919  nn0sscn  8186  qsscn  8566  serige0  9252  serile  9253  reexpcl  9272  rpexpcl  9274  reexpclzap  9275  expge0  9291  expge1  9292  abscn2  9835  recn2  9837  imcn2  9838  climabs  9840  climre  9842  climim  9843  iserile  9862  climserile  9865  climcvg1nlem  9868
  Copyright terms: Public domain W3C validator