Theorem rexr 8002

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7809   RR*cxr 7990

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-xr 7995

This theorem is referenced by:  rexri  8014  lenlt  8032  ltpnf  9779  mnflt  9782  xrltnsym  9792  xrlttr  9794  xrltso  9795  xrre  9819  xrre3  9821  xltnegi  9834  rexadd  9851  xaddnemnf  9856  xaddnepnf  9857  xaddcom  9860  xnegdi  9867  xpncan  9870  xnpcan  9871  xleadd1a  9872  xleadd1  9874  xltadd1  9875  xltadd2  9876  xsubge0  9880  xposdif  9881  elioo4g  9933  elioc2  9935  elico2  9936  elicc2  9937  iccss  9940  iooshf  9951  iooneg  9987  icoshft  9989  qbtwnxr  10257  modqmuladdim  10366  elicc4abs  11102  icodiamlt  11188  xrmaxrecl  11262  xrmaxaddlem  11267  xrminrecl  11280  bl2in  13873  blssps  13897  blss  13898  reopnap  14008  bl2ioo  14012  blssioo  14015  sincosq2sgn  14218  sincosq3sgn  14219  sincos6thpi  14233