Axiom ax-resscn 7384

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7296	. 2 class ℝ
2		cc 7295	. 2 class ℂ
3	1, 2	wss 2988	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  7422  reex  7423  recni  7447  nnsscn  8365  nn0sscn  8614  qsscn  9051  serige0  9854  serile  9855  reexpcl  9874  rpexpcl  9876  reexpclzap  9877  expge0  9893  expge1  9894  abscn2  10600  recn2  10602  imcn2  10603  climabs  10605  climre  10607  climim  10608  iserile  10627  climserile  10630  climcvg1nlem  10633  fsumrecl  10683  fsumrpcl  10686