Axiom ax-resscn 7200

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7160. (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 7112	. 2 class RR
2		cc 7111	. 2 class CC
3	1, 2	wss 2982	1 wff RR C_ CC

This axiom is referenced by:  recn  7238  reex  7239  recni  7263  nnsscn  8181  nn0sscn  8430  qsscn  8867  serige0  9640  serile  9641  reexpcl  9660  rpexpcl  9662  reexpclzap  9663  expge0  9679  expge1  9680  abscn2  10372  recn2  10374  imcn2  10375  climabs  10377  climre  10379  climim  10380  iserile  10399  climserile  10402  climcvg1nlem  10405