Theorem rpred 9919

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8019  ℝ⁺crp 9876

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 3204  df-ss 3211  df-rp 9877

This theorem is referenced by:  rpxrd  9920  rpcnd  9921  rpregt0d  9926  rprege0d  9927  rprene0d  9928  rprecred  9931  ltmulgt11d  9955  ltmulgt12d  9956  gt0divd  9957  ge0divd  9958  lediv12ad  9979  ltexp2a  10841  leexp2a  10842  expnlbnd2  10915  cvg1nlemcxze  11530  cvg1nlemcau  11532  cvg1nlemres  11533  cvg1n  11534  resqrexlemp1rp  11554  resqrexlemfp1  11557  resqrexlemover  11558  resqrexlemdec  11559  resqrexlemdecn  11560  resqrexlemlo  11561  resqrexlemcalc1  11562  resqrexlemcalc2  11563  resqrexlemcalc3  11564  resqrexlemnmsq  11565  resqrexlemnm  11566  resqrexlemcvg  11567  resqrexlemgt0  11568  resqrexlemoverl  11569  resqrexlemglsq  11570  resqrexlemga  11571  cau3lem  11662  bdtrilem  11787  bdtri  11788  addcn2  11858  mulcn2  11860  reccn2ap  11861  climrecvg1n  11896  climcvg1nlem  11897  isumrpcl  12042  expcnvap0  12050  absgtap  12058  cvgratnnlemsumlt  12076  cvgratnnlemfm  12077  cvgratnnlemrate  12078  mertenslemi1  12083  effsumlt  12240  eirraplem  12325  bitsmod  12504  4sqlem7  12944  ssblex  15142  metss2lem  15208  addcncntoplem  15272  mulcncflem  15318  ivthinclemlopn  15347  ivthinclemuopn  15349  limcimolemlt  15375  limcimo  15376  cnplimclemle  15379  limccnp2lem  15387  dveflem  15437  efltlemlt  15485  pilem3  15494  cxplt  15627  cxple  15628  rpcxple2  15629  rpcxplt2  15630  rpcxpsqrt  15633  rpabscxpbnd  15651  logbgt0b  15677  logbgcd1irr  15678  logbgcd1irraplemexp  15679  qdencn  16541  cvgcmp2nlemabs  16546  iooref1o  16548  trilpolemclim  16550  trilpolemisumle  16552  trilpolemeq1  16554  nconstwlpolemgt0  16578  taupi  16587