Theorem elrp 13059

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 5170	. 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2		df-rp 13058	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
3	1, 2	elrab2 3711	1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183  0cc0 11184   < clt 11324  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-rp 13058

This theorem is referenced by:  elrpii  13060  nnrp  13068  rpgt0  13069  rpregt0  13071  ralrp  13077  rexrp  13078  rpaddcl  13079  rpmulcl  13080  rpdivcl  13082  rpgecl  13085  rphalflt  13086  ge0p1rp  13088  rpneg  13089  negelrp  13090  ltsubrp  13093  ltaddrp  13094  difrp  13095  elrpd  13096  infmrp1  13406  dfrp2  13456  iccdil  13550  icccntr  13552  1mod  13954  expgt0  14146  resqrex  15299  sqrtdiv  15314  sqrtneglem  15315  mulcn2  15642  ef01bndlem  16232  sinltx  16237  met1stc  24555  met2ndci  24556  bcthlem4  25380  itg2mulc  25802  dvferm1  26043  dvne0  26070  reeff1o  26509  ellogdm  26699  cxpge0  26743  cxple2a  26759  cxpcn3lem  26808  cxpaddlelem  26812  cxpaddle  26813  atanbnd  26987  rlimcnp  27026  amgm  27052  chtub  27274  chebbnd1  27534  chto1ub  27538  pntlem3  27671  blocni  30837  rpdp2cl  32846  dp2ltc  32851  dplti  32869  dpgti  32870  dpexpp1  32872  dpmul4  32878  fdvposlt  34576  hgt750lem  34628  unbdqndv2lem2  36476  heiborlem8  37778  dvrelog2  42021  dvrelog3  42022  2xp3dxp2ge1d  42198  sqrtcvallem1  43593  wallispilem4  45989  perfectALTVlem2  47596  regt1loggt0  48270