Theorem rpred 9790

Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem rpred

Step	Hyp	Ref	Expression
1		rpssre 9758	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3182	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7897  ℝ⁺crp 9747

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-in 3163  df-ss 3170  df-rp 9748

This theorem is referenced by:  rpxrd  9791  rpcnd  9792  rpregt0d  9797  rprege0d  9798  rprene0d  9799  rprecred  9802  ltmulgt11d  9826  ltmulgt12d  9827  gt0divd  9828  ge0divd  9829  lediv12ad  9850  ltexp2a  10702  leexp2a  10703  expnlbnd2  10776  cvg1nlemcxze  11166  cvg1nlemcau  11168  cvg1nlemres  11169  cvg1n  11170  resqrexlemp1rp  11190  resqrexlemfp1  11193  resqrexlemover  11194  resqrexlemdec  11195  resqrexlemdecn  11196  resqrexlemlo  11197  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrexlemcalc3  11200  resqrexlemnmsq  11201  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemgt0  11204  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  cau3lem  11298  bdtrilem  11423  bdtri  11424  addcn2  11494  mulcn2  11496  reccn2ap  11497  climrecvg1n  11532  climcvg1nlem  11533  isumrpcl  11678  expcnvap0  11686  absgtap  11694  cvgratnnlemsumlt  11712  cvgratnnlemfm  11713  cvgratnnlemrate  11714  mertenslemi1  11719  effsumlt  11876  eirraplem  11961  bitsmod  12140  4sqlem7  12580  ssblex  14775  metss2lem  14841  addcncntoplem  14905  mulcncflem  14951  ivthinclemlopn  14980  ivthinclemuopn  14982  limcimolemlt  15008  limcimo  15009  cnplimclemle  15012  limccnp2lem  15020  dveflem  15070  efltlemlt  15118  pilem3  15127  cxplt  15260  cxple  15261  rpcxple2  15262  rpcxplt2  15263  rpcxpsqrt  15266  rpabscxpbnd  15284  logbgt0b  15310  logbgcd1irr  15311  logbgcd1irraplemexp  15312  qdencn  15784  cvgcmp2nlemabs  15789  iooref1o  15791  trilpolemclim  15793  trilpolemisumle  15795  trilpolemeq1  15797  nconstwlpolemgt0  15821  taupi  15830