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	$$⊢ℝ\subseteq ℂ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr	$$classℝ$$
1		cc	$$classℂ$$
2	0 1	wss	$$wffℝ\subseteq ℂ$$