Theorem rexr 7729

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

Syntax hints:   -> wi 4   e. wcel 1461   RRcr 7540   RR*cxr 7717

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-xr 7722

This theorem is referenced by:  rexri  7741  lenlt  7757  ltpnf  9454  mnflt  9456  xrltnsym  9466  xrlttr  9468  xrltso  9469  xrre  9490  xrre3  9492  xltnegi  9505  rexadd  9522  xaddnemnf  9527  xaddnepnf  9528  xaddcom  9531  xnegdi  9538  xpncan  9541  xnpcan  9542  xleadd1a  9543  xleadd1  9545  xltadd1  9546  xltadd2  9547  xsubge0  9551  xposdif  9552  elioo4g  9604  elioc2  9606  elico2  9607  elicc2  9608  iccss  9611  iooshf  9622  iooneg  9658  icoshft  9660  qbtwnxr  9922  modqmuladdim  10027  elicc4abs  10752  icodiamlt  10838  xrmaxrecl  10910  xrmaxaddlem  10915  xrminrecl  10928  bl2in  12386  blssps  12410  blss  12411  bl2ioo  12522  blssioo  12525