Theorem rpred 9900

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 9868	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3222	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8006  ℝ⁺crp 9857

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-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210  df-rp 9858

This theorem is referenced by:  rpxrd  9901  rpcnd  9902  rpregt0d  9907  rprege0d  9908  rprene0d  9909  rprecred  9912  ltmulgt11d  9936  ltmulgt12d  9937  gt0divd  9938  ge0divd  9939  lediv12ad  9960  ltexp2a  10821  leexp2a  10822  expnlbnd2  10895  cvg1nlemcxze  11501  cvg1nlemcau  11503  cvg1nlemres  11504  cvg1n  11505  resqrexlemp1rp  11525  resqrexlemfp1  11528  resqrexlemover  11529  resqrexlemdec  11530  resqrexlemdecn  11531  resqrexlemlo  11532  resqrexlemcalc1  11533  resqrexlemcalc2  11534  resqrexlemcalc3  11535  resqrexlemnmsq  11536  resqrexlemnm  11537  resqrexlemcvg  11538  resqrexlemgt0  11539  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemga  11542  cau3lem  11633  bdtrilem  11758  bdtri  11759  addcn2  11829  mulcn2  11831  reccn2ap  11832  climrecvg1n  11867  climcvg1nlem  11868  isumrpcl  12013  expcnvap0  12021  absgtap  12029  cvgratnnlemsumlt  12047  cvgratnnlemfm  12048  cvgratnnlemrate  12049  mertenslemi1  12054  effsumlt  12211  eirraplem  12296  bitsmod  12475  4sqlem7  12915  ssblex  15113  metss2lem  15179  addcncntoplem  15243  mulcncflem  15289  ivthinclemlopn  15318  ivthinclemuopn  15320  limcimolemlt  15346  limcimo  15347  cnplimclemle  15350  limccnp2lem  15358  dveflem  15408  efltlemlt  15456  pilem3  15465  cxplt  15598  cxple  15599  rpcxple2  15600  rpcxplt2  15601  rpcxpsqrt  15604  rpabscxpbnd  15622  logbgt0b  15648  logbgcd1irr  15649  logbgcd1irraplemexp  15650  qdencn  16425  cvgcmp2nlemabs  16430  iooref1o  16432  trilpolemclim  16434  trilpolemisumle  16436  trilpolemeq1  16438  nconstwlpolemgt0  16462  taupi  16471