Axiom ax-resscn 7033

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6993. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-resscn	|- RR C_ CC

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 6945	. 2 class RR
2		cc 6944	. 2 class CC
3	1, 2	wss 2944	1 wff RR C_ CC

This axiom is referenced by:  recn  7071  reex  7072  recni  7096  nnsscn  7994  nn0sscn  8243  qsscn  8662  serige0  9416  serile  9417  reexpcl  9436  rpexpcl  9438  reexpclzap  9439  expge0  9455  expge1  9456  abscn2  10065  recn2  10067  imcn2  10068  climabs  10070  climre  10072  climim  10073  iserile  10092  climserile  10095  climcvg1nlem  10098