Axiom ax-resscn 8184

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 8140. (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 8091	. 2 class RR
2		cc 8090	. 2 class CC
3	1, 2	wss 3201	1 wff RR C_ CC

This axiom is referenced by:  recn  8225  reex  8226  recni  8251  rerecapb  9082  nnsscn  9207  nn0sscn  9466  qsscn  9926  reexpcl  10881  rpexpcl  10883  reexpclzap  10884  expge0  10900  expge1  10901  abscn2  11955  recn2  11957  imcn2  11958  climabs  11960  climre  11962  climim  11963  climcvg1nlem  11989  fsumrecl  12042  fsumrpcl  12045  fsumge0  12100  fsumre  12113  fsumim  12114  fprodrecl  12249  fprodrpcl  12252  fprodreclf  12255  fprodge0  12278  fprodge1  12280  reeff1  12341  remet  15359  tgioo2cntop  15368  tgioo2  15370  abscncf  15396  recncf  15397  imcncf  15398  cnrehmeocntop  15421  maxcncf  15426  mincncf  15427  ivthreinc  15456  hovercncf  15457  limcimolemlt  15475  recnprss  15498  dvidrelem  15503  dvidre  15508  dvcjbr  15519  dvfre  15521  reeff1olem  15582  cosz12  15591  ioocosf1o  15665