Theorem rexr 8003

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 8001	. 2 |- RR C_ RR*
2	1	sseli 3152	1 |- ( A e. RR -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7810   RR*cxr 7991

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-xr 7996

This theorem is referenced by:  rexri  8015  lenlt  8033  ltpnf  9780  mnflt  9783  xrltnsym  9793  xrlttr  9795  xrltso  9796  xrre  9820  xrre3  9822  xltnegi  9835  rexadd  9852  xaddnemnf  9857  xaddnepnf  9858  xaddcom  9861  xnegdi  9868  xpncan  9871  xnpcan  9872  xleadd1a  9873  xleadd1  9875  xltadd1  9876  xltadd2  9877  xsubge0  9881  xposdif  9882  elioo4g  9934  elioc2  9936  elico2  9937  elicc2  9938  iccss  9941  iooshf  9952  iooneg  9988  icoshft  9990  qbtwnxr  10258  modqmuladdim  10367  elicc4abs  11103  icodiamlt  11189  xrmaxrecl  11263  xrmaxaddlem  11268  xrminrecl  11281  bl2in  13906  blssps  13930  blss  13931  reopnap  14041  bl2ioo  14045  blssioo  14048  sincosq2sgn  14251  sincosq3sgn  14252  sincos6thpi  14266