Axiom ax-resscn

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

	Ref	Expression
Assertion	ax-resscn	|- RR C_ CC

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr	|- RR
1		cc	|- CC
2	0 1	wss	|- RR C_ CC