Theorem rexrd 8207

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 8201	. 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 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:  xnn0xr  9448  rpxr  9869  rpxrd  9905  xnn0dcle  10010  xnegcl  10040  xaddf  10052  xaddval  10053  xnn0lenn0nn0  10073  xposdif  10090  iooshf  10160  icoshftf1o  10199  ioo0  10491  ioom  10492  ico0  10493  ioc0  10494  xqltnle  10499  modqelico  10568  mulqaddmodid  10598  addmodid  10606  elicc4abs  11621  xrmaxiflemcl  11772  fprodge1  12166  pcxcl  12850  pcdvdsb  12859  pcaddlem  12878  pcadd  12879  xblss2ps  15094  xblss2  15095  blss2ps  15096  blss2  15097  blhalf  15098  cnblcld  15225  ioo2blex  15242  tgioo  15244  cnopnap  15301  suplociccreex  15314  suplociccex  15315  dedekindicc  15323  ivthinclemlm  15324  ivthinclemum  15325  ivthinclemlopn  15326  ivthinclemuopn  15328  ivthdec  15334  ivthreinc  15335  sin0pilem2  15472  pilem3  15473  vtxdgfifival  16051