Theorem rexr 8203

Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
rexr	|- ( A e. RR -> A e. RR* )

Proof of Theorem rexr

Step	Hyp	Ref	Expression
1		ressxr 8201	. 2 |- RR C_ RR*
2	1	sseli 3220	1 |- ( A e. RR -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8009   RR*cxr 8191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-xr 8196

This theorem is referenced by:  rexri  8215  lenlt  8233  ltpnf  9988  mnflt  9991  xrltnsym  10001  xrlttr  10003  xrltso  10004  xrre  10028  xrre3  10030  xltnegi  10043  rexadd  10060  xaddnemnf  10065  xaddnepnf  10066  xaddcom  10069  xnegdi  10076  xpncan  10079  xnpcan  10080  xleadd1a  10081  xleadd1  10083  xltadd1  10084  xltadd2  10085  xsubge0  10089  xposdif  10090  elioo4g  10142  elioc2  10144  elico2  10145  elicc2  10146  iccss  10149  iooshf  10160  iooneg  10196  icoshft  10198  qbtwnxr  10489  modqmuladdim  10601  elicc4abs  11620  icodiamlt  11706  xrmaxrecl  11781  xrmaxaddlem  11786  xrminrecl  11799  bl2in  15092  blssps  15116  blss  15117  reopnap  15235  bl2ioo  15239  blssioo  15242  sincosq2sgn  15516  sincosq3sgn  15517  sincos6thpi  15531