Theorem elrpii 11949

Description: Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)

Hypotheses

Ref	Expression
elrpi.1	⊢ 𝐴 ∈ ℝ
elrpi.2	⊢ 0 < 𝐴

Assertion

Ref	Expression
elrpii	⊢ 𝐴 ∈ ℝ+

Proof of Theorem elrpii

Step	Hyp	Ref	Expression
1		elrpi.1	. 2 ⊢ 𝐴 ∈ ℝ
2		elrpi.2	. 2 ⊢ 0 < 𝐴
3		elrp 11948	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	mpbir2an 993	1 ⊢ 𝐴 ∈ ℝ+

Syntax hints:   ∈ wcel 2103   class class class wbr 4760  ℝcr 10048  0cc0 10049   < clt 10187  ℝ⁺crp 11946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-br 4761  df-rp 11947

This theorem is referenced by:  1rp  11950  2rp  11951  3rp  11952  iexpcyc  13084  discr  13116  sqrlem7  14109  caurcvgr  14524  epr  15056  aaliou3lem1  24217  aaliou3lem2  24218  aaliou3lem3  24219  pirp  24333  pige3  24389  cosordlem  24397  efif1olem2  24409  cxpsqrtlem  24568  log2cnv  24791  cht3  25019  chtublem  25056  chtub  25057  bposlem6  25134  lgsdir2lem1  25170  lgsdir2lem4  25173  lgsdir2lem5  25174  2sqlem11  25274  chebbnd1lem3  25280  chebbnd1  25281  chto1ub  25285  dchrvmasumiflem1  25310  pntlemg  25407  pntlemr  25411  pntlemf  25414  minvecolem3  27962  dp2lt10  29821  ballotlem2  30780  pigt3  33634  cntotbnd  33827  heiborlem5  33846  heiborlem7  33848  isosctrlem1ALT  39586  sineq0ALT  39589  limclner  40303  stoweidlem5  40642  stoweidlem28  40665  stoweidlem59  40696  stoweid  40700  stirlinglem12  40722  fourierswlem  40867  fouriersw  40868