Axiom ax-resscn 7866

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

This axiom is referenced by:  recn  7907  reex  7908  recni  7932  nnsscn  8883  nn0sscn  9140  qsscn  9590  reexpcl  10493  rpexpcl  10495  reexpclzap  10496  expge0  10512  expge1  10513  abscn2  11278  recn2  11280  imcn2  11281  climabs  11283  climre  11285  climim  11286  climcvg1nlem  11312  fsumrecl  11364  fsumrpcl  11367  fsumge0  11422  fsumre  11435  fsumim  11436  fprodrecl  11571  fprodrpcl  11574  fprodreclf  11577  fprodge0  11600  fprodge1  11602  reeff1  11663  remet  13334  tgioo2cntop  13343  abscncf  13366  recncf  13367  imcncf  13368  cnrehmeocntop  13387  limcimolemlt  13427  recnprss  13450  dvcjbr  13466  dvfre  13468  reeff1olem  13486  cosz12  13495  ioocosf1o  13569