Theorem elrp 12392

Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)

Assertion

Ref	Expression
elrp	⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Proof of Theorem elrp

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5070	. 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2		df-rp 12391	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
3	1, 2	elrab2 3683	1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536  0cc0 10537   < clt 10675  ℝ⁺crp 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-rp 12391

This theorem is referenced by:  elrpii  12393  nnrp  12401  rpgt0  12402  rpregt0  12404  ralrp  12410  rexrp  12411  rpaddcl  12412  rpmulcl  12413  rpdivcl  12415  rpgecl  12418  rphalflt  12419  ge0p1rp  12421  rpneg  12422  negelrp  12423  ltsubrp  12426  ltaddrp  12427  difrp  12428  elrpd  12429  infmrp1  12738  iccdil  12877  icccntr  12879  1mod  13272  expgt0  13463  resqrex  14610  sqrtdiv  14625  sqrtneglem  14626  mulcn2  14952  ef01bndlem  15537  sinltx  15542  met1stc  23131  met2ndci  23132  bcthlem4  23930  itg2mulc  24348  dvferm1  24582  dvne0  24608  reeff1o  25035  ellogdm  25222  cxpge0  25266  cxple2a  25282  cxpcn3lem  25328  cxpaddlelem  25332  cxpaddle  25333  atanbnd  25504  rlimcnp  25543  amgm  25568  chtub  25788  chebbnd1  26048  chto1ub  26052  pntlem3  26185  blocni  28582  dfrp2  30491  rpdp2cl  30558  dp2ltc  30563  dplti  30581  dpgti  30582  dpexpp1  30584  dpmul4  30590  fdvposlt  31870  hgt750lem  31922  unbdqndv2lem2  33849  heiborlem8  35111  2xp3dxp2ge1d  39117  wallispilem4  42373  perfectALTVlem2  43907  regt1loggt0  44616