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

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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 6886 . 2 class
2 cc 6885 . 2 class
31, 2wss 2917 1 wff ℝ ⊆ ℂ
Colors of variables: wff set class
This axiom is referenced by:  recn  7012  reex  7013  recni  7037  nnsscn  7917  nn0sscn  8184  qsscn  8564  serige0  9226  serile  9227  reexpcl  9246  rpexpcl  9248  reexpclzap  9249  expge0  9265  expge1  9266  abscn2  9808  recn2  9810  imcn2  9811  climabs  9813  climre  9815  climim  9816  iserile  9835  climserile  9838  climcvg1nlem  9841
  Copyright terms: Public domain W3C validator