Theorem rpred 9909

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  ℝ⁺crp 9866

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 9867

This theorem is referenced by:  rpxrd  9910  rpcnd  9911  rpregt0d  9916  rprege0d  9917  rprene0d  9918  rprecred  9921  ltmulgt11d  9945  ltmulgt12d  9946  gt0divd  9947  ge0divd  9948  lediv12ad  9969  ltexp2a  10830  leexp2a  10831  expnlbnd2  10904  cvg1nlemcxze  11514  cvg1nlemcau  11516  cvg1nlemres  11517  cvg1n  11518  resqrexlemp1rp  11538  resqrexlemfp1  11541  resqrexlemover  11542  resqrexlemdec  11543  resqrexlemdecn  11544  resqrexlemlo  11545  resqrexlemcalc1  11546  resqrexlemcalc2  11547  resqrexlemcalc3  11548  resqrexlemnmsq  11549  resqrexlemnm  11550  resqrexlemcvg  11551  resqrexlemgt0  11552  resqrexlemoverl  11553  resqrexlemglsq  11554  resqrexlemga  11555  cau3lem  11646  bdtrilem  11771  bdtri  11772  addcn2  11842  mulcn2  11844  reccn2ap  11845  climrecvg1n  11880  climcvg1nlem  11881  isumrpcl  12026  expcnvap0  12034  absgtap  12042  cvgratnnlemsumlt  12060  cvgratnnlemfm  12061  cvgratnnlemrate  12062  mertenslemi1  12067  effsumlt  12224  eirraplem  12309  bitsmod  12488  4sqlem7  12928  ssblex  15126  metss2lem  15192  addcncntoplem  15256  mulcncflem  15302  ivthinclemlopn  15331  ivthinclemuopn  15333  limcimolemlt  15359  limcimo  15360  cnplimclemle  15363  limccnp2lem  15371  dveflem  15421  efltlemlt  15469  pilem3  15478  cxplt  15611  cxple  15612  rpcxple2  15613  rpcxplt2  15614  rpcxpsqrt  15617  rpabscxpbnd  15635  logbgt0b  15661  logbgcd1irr  15662  logbgcd1irraplemexp  15663  qdencn  16509  cvgcmp2nlemabs  16514  iooref1o  16516  trilpolemclim  16518  trilpolemisumle  16520  trilpolemeq1  16522  nconstwlpolemgt0  16546  taupi  16555