Axiom ax-resscn 7855

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7811. (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 7762	. 2 class RR
2		cc 7761	. 2 class CC
3	1, 2	wss 3121	1 wff RR C_ CC

This axiom is referenced by:  recn  7896  reex  7897  recni  7921  nnsscn  8872  nn0sscn  9129  qsscn  9579  reexpcl  10482  rpexpcl  10484  reexpclzap  10485  expge0  10501  expge1  10502  abscn2  11267  recn2  11269  imcn2  11270  climabs  11272  climre  11274  climim  11275  climcvg1nlem  11301  fsumrecl  11353  fsumrpcl  11356  fsumge0  11411  fsumre  11424  fsumim  11425  fprodrecl  11560  fprodrpcl  11563  fprodreclf  11566  fprodge0  11589  fprodge1  11591  reeff1  11652  remet  13295  tgioo2cntop  13304  abscncf  13327  recncf  13328  imcncf  13329  cnrehmeocntop  13348  limcimolemlt  13388  recnprss  13411  dvcjbr  13427  dvfre  13429  reeff1olem  13447  cosz12  13456  ioocosf1o  13530