Theorem rexrd 8196

Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rexrd.1	|- ( ph -> A e. RR )

Assertion

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

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 8190	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sselid 3222	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   RR*cxr 8180

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 8185

This theorem is referenced by:  xnn0xr  9437  rpxr  9857  rpxrd  9893  xnn0dcle  9998  xnegcl  10028  xaddf  10040  xaddval  10041  xnn0lenn0nn0  10061  xposdif  10078  iooshf  10148  icoshftf1o  10187  ioo0  10479  ioom  10480  ico0  10481  ioc0  10482  xqltnle  10487  modqelico  10556  mulqaddmodid  10586  addmodid  10594  elicc4abs  11605  xrmaxiflemcl  11756  fprodge1  12150  pcxcl  12834  pcdvdsb  12843  pcaddlem  12862  pcadd  12863  xblss2ps  15078  xblss2  15079  blss2ps  15080  blss2  15081  blhalf  15082  cnblcld  15209  ioo2blex  15226  tgioo  15228  cnopnap  15285  suplociccreex  15298  suplociccex  15299  dedekindicc  15307  ivthinclemlm  15308  ivthinclemum  15309  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthdec  15318  ivthreinc  15319  sin0pilem2  15456  pilem3  15457