Axiom ax-resscn 7534

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

This axiom is referenced by:  recn  7572  reex  7573  recni  7597  nnsscn  8525  nn0sscn  8776  qsscn  9215  reexpcl  10087  rpexpcl  10089  reexpclzap  10090  expge0  10106  expge1  10107  abscn2  10858  recn2  10860  imcn2  10861  climabs  10863  climre  10865  climim  10866  climcvg1nlem  10892  fsumrecl  10944  fsumrpcl  10947  fsumge0  11002  fsumre  11015  fsumim  11016  reeff1  11140  remet  12314  abscncf  12338  recncf  12339  imcncf  12340