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	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr	⊢ ℝ
1		cc	⊢ ℂ
2	0 1	wss	⊢ ℝ ⊆ ℂ